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.
Every formula in classical logic is logically equivalent to a formula in prenex normal form.
are quantifier-free formulas with the free variables shown then is in prenex normal form with matrix
, while is logically equivalent but not in prenex normal form.
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 and The equivalences are valid when
For example, in the language of rings, but 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.
and then put in prenex normal form
The rules for negation say that and 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
and applying the rules for disjunction and negation 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): The rules for removing quantifiers from the consequent are: For example, when the range of quantification is the non-negative natural number (viz.
The latter statement says that there exists some natural number n such that if x is less than n, then x is less than zero.
The latter statement is true because n=0 makes the implication a tautology.
Note that the placement of brackets implies the scope of the quantification, which is very important for the meaning of the formula.
The latter statement says that if there exists some natural number n such that x is less than n, then x is less than zero.
The latter statement doesn't hold for x=1, because the natural number n=2 satisfies x Consider the formula By recursively applying the rules starting at the innermost subformulas, the following sequence of logically equivalent formulas can be obtained: 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 can be obtained: The ordering of the two universal quantifier with the same scope doesn't change the meaning/truth value of the statement. 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 BHK interpretation illustrates why some formulas have no intuitionistically-equivalent prenex form. The rules for converting a formula to prenex form that do fail in intuitionistic logic are: (x does not appear as a free variable of Some proof calculi will only deal with a theory whose formulae are written in prenex normal form. 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 This fact allowed Tarski to prove that Euclidean geometry is decidable.