Prenex normal form

The rules for conjunction and disjunction say that

${\displaystyle (\forall x\phi )\land \psi }$ is equivalent to ${\displaystyle \forall x(\phi \land \psi )}$ under (mild) additional condition ${\displaystyle \exists x\top }$, or, equivalently, ${\displaystyle \lnot \forall x\bot }$ (meaning that at least one individual exists),

${\displaystyle (\forall x\phi )\lor \psi }$ is equivalent to ${\displaystyle \forall x(\phi \lor \psi )}$;

and

${\displaystyle (\exists x\phi )\land \psi }$ is equivalent to ${\displaystyle \exists x(\phi \land \psi )}$,

${\displaystyle (\exists x\phi )\lor \psi }$ is equivalent to ${\displaystyle \exists x(\phi \lor \psi )}$ under additional condition ${\displaystyle \exists x\top }$.

The equivalences are valid when ${\displaystyle x}$ does not appear as a free variable of ${\displaystyle \psi }$; if ${\displaystyle x}$ does appear free in ${\displaystyle \psi }$, one can rename the bound ${\displaystyle x}$ in ${\displaystyle (\exists x\phi )}$ and obtain the equivalent ${\displaystyle (\exists x'\phi [x/x'])}$.

For example, in the language of rings,

${\displaystyle (\exists x(x^{2}=1))\land (0=y)}$ is equivalent to ${\displaystyle \exists x(x^{2}=1\land 0=y)}$,

but

${\displaystyle (\exists x(x^{2}=1))\land (0=x)}$ is not equivalent to ${\displaystyle \exists x(x^{2}=1\land 0=x)}$

because the formula on the left is true in any ring when the free variable x is equal to 0, while the formula on the right has no free variables and is false in any nontrivial ring. So ${\displaystyle (\exists x(x^{2}=1))\land (0=x)}$ will be first rewritten as ${\displaystyle (\exists x'(x'^{2}=1))\land (0=x)}$ and then put in prenex normal form ${\displaystyle \exists x'(x'^{2}=1\land 0=x)}$.

The rules for negation say that

${\displaystyle \lnot \exists x\phi }$ is equivalent to ${\displaystyle \forall x\lnot \phi }$

and

${\displaystyle \lnot \forall x\phi }$ is equivalent to ${\displaystyle \exists x\lnot \phi }$.

There are four rules for implication: two that remove quantifiers from the antecedent and two that remove quantifiers from the consequent. These rules can be derived by rewriting the implication ${\displaystyle \phi \rightarrow \psi }$ as ${\displaystyle \lnot \phi \lor \psi }$ and applying the rules for disjunction above. As with the rules for disjunction, these rules require that the variable quantified in one subformula does not appear free in the other subformula.

The rules for removing quantifiers from the antecedent are (note the change of quantifiers):

${\displaystyle (\forall x\phi )\rightarrow \psi }$ is equivalent to ${\displaystyle \exists x(\phi \rightarrow \psi )}$ (under the assumption that ${\displaystyle \exists x\top }$),

${\displaystyle (\exists x\phi )\rightarrow \psi }$ is equivalent to ${\displaystyle \forall x(\phi \rightarrow \psi )}$.

The rules for removing quantifiers from the consequent are:

${\displaystyle \phi \rightarrow (\exists x\psi )}$ is equivalent to ${\displaystyle \exists x(\phi \rightarrow \psi )}$ (under the assumption that ${\displaystyle \exists x\top }$),

${\displaystyle \phi \rightarrow (\forall x\psi )}$ is equivalent to ${\displaystyle \forall x(\phi \rightarrow \psi )}$.

Suppose that ${\displaystyle \phi }$, ${\displaystyle \psi }$, and ${\displaystyle \rho }$ are quantifier-free formulas and no two of these formulas share any free variable. Consider the formula

${\displaystyle (\phi \lor \exists x\psi )\rightarrow \forall z\rho }$.

By recursively applying the rules starting at the innermost subformulas, the following sequence of logically equivalent formulas can be obtained:

${\displaystyle (\phi \lor \exists x\psi )\rightarrow \forall z\rho }$.

${\displaystyle (\exists x(\phi \lor \psi ))\rightarrow \forall z\rho }$,

${\displaystyle \neg (\exists x(\phi \lor \psi ))\lor \forall z\rho }$,

${\displaystyle (\forall x\neg (\phi \lor \psi ))\lor \forall z\rho }$,

${\displaystyle \forall x(\neg (\phi \lor \psi )\lor \forall z\rho )}$,

${\displaystyle \forall x((\phi \lor \psi )\rightarrow \forall z\rho )}$,

${\displaystyle \forall x(\forall z((\phi \lor \psi )\rightarrow \rho ))}$,

${\displaystyle \forall x\forall z((\phi \lor \psi )\rightarrow \rho )}$.

This is not the only prenex form equivalent to the original formula. For example, by dealing with the consequent before the antecedent in the example above, the prenex form

${\displaystyle \forall z\forall x((\phi \lor \psi )\rightarrow \rho )}$

can be obtained:

${\displaystyle \forall z((\phi \lor \exists x\psi )\rightarrow \rho )}$

${\displaystyle \forall z((\exists x(\phi \lor \psi ))\rightarrow \rho )}$,

${\displaystyle \forall z(\forall x((\phi \lor \psi )\rightarrow \rho ))}$,

${\displaystyle \forall z\forall x((\phi \lor \psi )\rightarrow \rho )}$.

The rules for converting a formula to prenex form make heavy use of classical logic. In intuitionistic logic, it is not true that every formula is logically equivalent to a prenex formula. The negation connective is one obstacle, but not the only one. The implication operator is also treated differently in intuitionistic logic than classical logic; in intuitionistic logic, it is not definable using disjunction and negation.

The BHK interpretation illustrates why some formulas have no intuitionistically-equivalent prenex form. In this interpretation, a proof of

${\displaystyle (\exists x\phi )\rightarrow \exists y\psi \qquad (1)}$

is a function which, given a concrete x and a proof of ${\displaystyle \phi (x)}$, produces a concrete y and a proof of ${\displaystyle \psi (y)}$. In this case it is allowable for the value of y to be computed from the given value of x. A proof of

${\displaystyle \exists y(\exists x\phi \rightarrow \psi ),\qquad (2)}$

on the other hand, produces a single concrete value of y and a function that converts any proof of ${\displaystyle \exists x\phi }$ into a proof of ${\displaystyle \psi (y)}$. If each x satisfying ${\displaystyle \phi }$ can be used to construct a y satisfying ${\displaystyle \psi }$ but no such y can be constructed without knowledge of such an x then formula (1) will not be equivalent to formula (2).

The rules for converting a formula to prenex form that do fail in intuitionistic logic are:

(1) ${\displaystyle \forall x(\phi \lor \psi )}$ implies ${\displaystyle (\forall x\phi )\lor \psi }$,

(2) ${\displaystyle \forall x(\phi \lor \psi )}$ implies ${\displaystyle \phi \lor (\forall x\psi )}$,

(3) ${\displaystyle (\forall x\phi )\rightarrow \psi }$ implies ${\displaystyle \exists x(\phi \rightarrow \psi )}$,

(4) ${\displaystyle \phi \rightarrow (\exists x\psi )}$ implies ${\displaystyle \exists x(\phi \rightarrow \psi )}$,

(5) ${\displaystyle \lnot \forall x\phi }$ implies ${\displaystyle \exists x\lnot \phi }$,

(x does not appear as a free variable of ${\displaystyle \,\psi }$ in (1) and (3); x does not appear as a free variable of ${\displaystyle \,\phi }$ in (2) and (4)).