QUANTIFICATION ::= quantification QUANTIFIER VAR-DECL+ FORMULA QUANTIFIER ::= forall | exists | exists-uniquely
A quantification with the forall quantifier is written:
forall VD_1; ...; VD_n · 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 VD_1; ...; VD_n · F
A quantification with the exists-uniquely quantifier is written:
exists ! VD_1; ...; VD_n · 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 VD_1; ...; VD_n · F is equivalent to forall VD_1 · ...forall VD_n · F; and forall V1, ..., Vn : S · F is equivalent to forall V1 : S · ...forall Vn : 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).