QUANTIFICATION ::= quantification QUANTIFIER VAR-DECL+ FORMULA
QUANTIFIER ::= universal | existential | unique-existential
A quantification with the universal 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 existential quantifier is written:
exists VD1; ...;VDn · F
A quantification with the unique-existential 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 some 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 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). Note that the body of a quantification extends as far as possible.