**Go up to** 2.3 Axioms

**Go forward to** 2.3.2 Logical Connectives

### 2.3.1 Quantifications

QUANTIFICATION ::= quantification QUANTIFIER VAR-DECL+ FORMULA
QUANTIFIER ::= forall | exists | exists-uniquely

A quantification with the `forall` quantifier is written:

*forall **VD*_{1}; ...; *VD*_{n} **·** *F*

The 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} **·** *F*

The 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
**[CHANGED:]** 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 **VD*_{1}; ...;
*VD*_{n} **·** *F* is equivalent to
*forall **VD*_{1} **·** ...forall *VD*_{n} **·** *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).

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk