A formula of the predicate calculus is in prenex[1] normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier-free part, called the matrix.[2] Together with the normal forms in propositional logic (e.g. disjunctive normal form or conjunctive normal form), it provides a canonical normal form useful in automated theorem proving.
Every formula in classical logic is logically equivalent to a formula in prenex normal form. For example, if
\phi(y)
\psi(z)
\rho(x)
\forallx\existsy\forallz(\phi(y)\lor(\psi(z) → \rho(x)))
\phi(y)\lor(\psi(z) → \rho(x))
\forallx((\existsy\phi(y))\lor((\existsz\psi(z)) → \rho(x)))
Every first-order formula is logically equivalent (in classical logic) to some formula in prenex normal form.[3] There are several conversion rules that can be recursively applied to convert a formula to prenex normal form. The rules depend on which logical connectives appear in the formula.
The rules for conjunction and disjunction say that
(\forallx\phi)\land\psi
\forallx(\phi\land\psi)
\existsx\top
lnot\forallx\bot
(\forallx\phi)\lor\psi
\forallx(\phi\lor\psi)
(\existsx\phi)\land\psi
\existsx(\phi\land\psi)
(\existsx\phi)\lor\psi
\existsx(\phi\lor\psi)
\existsx\top
x
\psi
x
\psi
x
(\existsx\phi)
(\existsx'\phi[x/x'])
For example, in the language of rings,
(\existsx(x2=1))\land(0=y)
\existsx(x2=1\land0=y)
(\existsx(x2=1))\land(0=x)
\existsx(x2=1\land0=x)
(\existsx(x2=1))\land(0=x)
(\existsx'(x'2=1))\land(0=x)
\existsx'(x'2=1\land0=x)
The rules for negation say that
lnot\existsx\phi
\forallxlnot\phi
lnot\forallx\phi
\existsxlnot\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
\phi → \psi
lnot\phi\lor\psi
The rules for removing quantifiers from the antecedent are (note the change of quantifiers):
(\forallx\phi) → \psi
\existsx(\phi → \psi)
\existsx\top
(\existsx\phi) → \psi
\forallx(\phi → \psi)
\phi → (\existsx\psi)
\existsx(\phi → \psi)
\existsx\top
\phi → (\forallx\psi)
\forallx(\phi → \psi)
n\inN
[\foralln\inN(x<n)] → (x<0)
\existsn\inN[(x<n) → (x<0)]
Note that the placement of brackets implies the scope of the quantification, which is very important for the meaning of the formula. Consider the following two statements:
\foralln\inN[(x<n) → (x<0)]
[\existsn\inN(x<n)] → (x<0)
Suppose that
\phi
\psi
\rho
(\phi\lor\existsx\psi) → \forallz\rho
(\phi\lor\existsx\psi) → \forallz\rho
(\existsx(\phi\lor\psi)) → \forallz\rho
\neg(\existsx(\phi\lor\psi))\lor\forallz\rho
(\forallx\neg(\phi\lor\psi))\lor\forallz\rho
\forallx(\neg(\phi\lor\psi)\lor\forallz\rho)
\forallx((\phi\lor\psi) → \forallz\rho)
\forallx(\forallz((\phi\lor\psi) → \rho))
\forallx\forallz((\phi\lor\psi) → \rho)
\forallz\forallx((\phi\lor\psi) → \rho)
\forallz((\phi\lor\existsx\psi) → \rho)
\forallz((\existsx(\phi\lor\psi)) → \rho)
\forallz(\forallx((\phi\lor\psi) → \rho))
\forallz\forallx((\phi\lor\psi) → \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
(\existsx\phi) → \existsy\psi (1)
\phi(x)
\psi(y)
\existsy(\existsx\phi → \psi), (2)
\existsx\phi
\psi(y)
\phi
\psi
The rules for converting a formula to prenex form that do fail in intuitionistic logic are:
(1)
\forallx(\phi\lor\psi)
(\forallx\phi)\lor\psi
(2)
\forallx(\phi\lor\psi)
\phi\lor(\forallx\psi)
(3)
(\forallx\phi) → \psi
\existsx(\phi → \psi)
(4)
\phi → (\existsx\psi)
\existsx(\phi → \psi)
(5)
lnot\forallx\phi
\existsxlnot\phi
\psi
\phi
Some proof calculi will only deal with a theory whose formulae are written in prenex normal form. The concept is essential for developing the arithmetical hierarchy and the analytical hierarchy.
Gödel's proof of his completeness theorem for first-order logic presupposes that all formulae have been recast in prenex normal form.
Tarski's axioms for geometry is a logical system whose sentences can all be written in universal–existential form, a special case of the prenex normal form that has every universal quantifier preceding any existential quantifier, so that all sentences can be rewritten in the form
\forallu
\forallv
\ldots
\existsa
\existsb
\phi
\phi