# LP, the Larch Prover -- Quantifiers

Terms and formulas in LP can contain existential and universal first-order
quantifiers. Examples:
`\A x \E y (x < y)
x < y => \E z (x < z /\ z < y)
`

The *existential quantifier* `\E x` is pronounced ``there exists an
`x`''. The *universal quantifier* `\A x` is pronounced ``for all
`x`''.
## Syntax

`<quantifier> ::= <quantifierSym> <variable>
<quantifierSym> ::= ``\A` | `\E`

## Examples

`\A x
\E i: Nat
`

## Usage

All quantified variables must have been declared previously in a
`declare variables` command.
The standard quantifier scope rules (from first-order logic) apply within terms
and formulas. The *scope* of the leading quantifier in the terms
`\A x t` and `\E x t` is the term `t`. An occurrence of a variable
in a term is *bound* if it is in the scope of a quantifier over that
variable; otherwise it is *free*. The free variables in a formula, rewrite
rule, or deduction rule are understood to be quantified universally. LP
suppresses the display of leading universal quantifiers.

LP uses the following hardwired rewrite rules to reduce terms containing
quantifiers.

`\A x t -> t
\E x t -> t
\E x \E x1 ... xn (x = t /\ P(x)) -> \E x1 ... \E xn P(t)
\A x \A x1 ... xn (~(x = t) \/ Q(x)) -> \A x1 ... xn Q(t)
\A x \A x1 ... xn (x = t /\ P(x) => Q(x)) -> \A x1 ... xn (P(t) => Q(t))
\A x \A x1 ... xn (P(x) => ~(x = t) \/ Q(x)) -> \A x1 ... xn (P(t) => Q(t))
`

Here `P(x)` and `Q(x)` are arbitrary terms, `t` is a term with no free
occurrences of `x`, and `P(t)` and `Q(t)` are the results of substituting
`t` for `x` in `P(x)` and `Q(x)` with appropriate changes of bound
variables to prevent a quantifier in `P` or `Q` from
capturing a variable in `t`.
The fix and instantiate commands, together with the
generalization and
specialization proof methods, enable
users to eliminate quantifiers from facts and conjectures.

See also prenex form.