# LP, the Larch Prover -- Prenex form

Every formula is logically equivalent to a prenex formula, that is, to a formula consisting of a string of quantifiers applied to a quantifier-free formula. For example, the following formulas are logically equivalent:
```\E w \A x P(w, x) => \A y \E z P(z, y)
\A w \A y \E x \E z (P(w, x) => P(z, y))
\A w \A y \E x (P(w, x) => P(x, y))
```
Every quantifier in a formula can be classified as a prenex-universal, a prenex-existential quantifier, or neither depending on whether it corresponds to a universal (\A) quantifier, an existential (\E) quantifier, or more than one quantifier in a systematically derived logically equivalent prenex formula. The leading quantifiers in \A x P and \E x P are prenex-universal and prenex-existential quantifiers, respectively. If a quantifier is prenex-universal (prenex-existential) in P, then it is the same in P /\ Q, P \/ Q, Q => P, \A y P, and \E y P; it is prenex-existential (prenex-universal) in ~P and P => Q; and it is neither in any other formula, e.g., in P <=> Q.

Formulas can be transformed systematically into prenex formulas using changes of bound variables and the following logical validities.

```\A x P         <=>  P                            (x not free in P)
\E x P         <=>  P                            (x not free in P)
\A x ~P        <=>  ~\E x P
\E x ~P        <=>  ~\A x P
\A x (P /\ Q)  <=>  \A x P /\ \A x Q
\E x (P /\ Q)  <=>  \E x P /\ Q                  (x not free in Q)
\A x (P \/ Q)  <=>  \A x P \/ Q                  (x not free in Q)
\E x (P \/ Q)  <=>  \E x P \/ \E x Q
\A x (P => Q)  <=>  \E x P) => Q                 (x not free in Q)
\A x (P => Q)  <=>  P => \A x Q                  (x not free in P)
\E x (P => Q)  <=>  \A x P => \E x Q
F(\A x P)      <=>  (F(true) /\ \A x P)
\/ (F(false) /\ ~\A x P)
```

The instantiate and fix commands enable users to eliminate certain prenex-universal and prenex-existential quantifiers from facts. The generalization and specialization proof methods provide the corresponding functionality for conjectures.