Prenex normal form
|
|
In predicate calculus, a formula is in prenex normal form if it can be 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 using the logical equivalence of formulas under the rewritings
- <math>\forall x ( P(x) \rightarrow Q ) \equiv \exists x P(x) \rightarrow Q<math>
and
- <math>\forall x ( P \rightarrow Q(x) ) \equiv P \rightarrow \forall x Q(x)<math>,
where <math>x<math> is free in <math>Q<math>, and their similar existential duals, and noting that via successive application of these rules all the quantifiers can be moved to the front of the 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.
Prenex normal forms are the main tool used by Gödel to prove his completeness theorem.