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.