Prenex normal form

From Wikipedia, the free encyclopedia

A formula of the predicate calculus is in prenex normal form if it is written as a string of quantifiers, followed by a quantifier-free part referred to as the matrix.

All first-order formulas are logically equivalent to some formula in prenex normal form. This can be shown by invoking the following schemata:

$\forall x ( P(x) \rightarrow Q ) \equiv \exists x P(x) \rightarrow Q$

and

$\forall x ( P \rightarrow Q(x) ) \equiv P \rightarrow \forall x Q(x)$ ,

The duals of these schemata, involving existential quantifiers, also hold. By successive application of these rules, all quantifiers can be moved to the far left of the formula. The result is the prenex normal form, logically equivalent to the initial formula.

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.