QUANTIFICATION ::= quantification QUANTIFIER VAR-DECL+ FORMULA QUANTIFIER ::= forall | exists | exists-uniquely
A quantification with the forall quantifier is written:
forall VD1; ...; VDn · FThe sign displayed as the `for all' symbol in LaTeX is input as `forall'. The sign displayed as ` · ' may be input as `·' in ISO Latin-1, or as `.' in ASCII.
A quantification with the exists quantifier is written:
exists VD1; ...;VDn · F
A quantification with the exists-uniquely quantifier is written:
exists ! VD1; ...;VDn · FThe sign displayed as the `exists' symbol in LaTeX is input as `exists'.
The first case is universal quantification, holding when the body F holds for all values of the quantified variables; the second case is existential quantification, holding when the body F holds for any values of the quantified variables; and the last case is unique existential quantification, abbreviating a formula that holds when the body F holds for unique values of the quantified variables.
The formula forall VD1; ...; VDn · F is equivalent to forall VD1 · ... forall VDn · F; and forall V_1, ..., V_n : S · F is equivalent to forall V_1 : S · ... forall V_n : S · F. Similarly for the other quantifiers. The scope of a variable declaration in a quantification is the component formula F, and an inner declaration for a variable with the same identifier as in an outer declaration overrides the outer declaration (regardless of whether the sorts of the variables are the same).