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.\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))
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.