A formula of the predicate calculus is in prenex normal form if it is written as a string of quantifiers (referred to as the prefix) followed by a quantifier-free part (referred to as the matrix).
Contents
- Conversion to prenex form
- Conjunction and disjunction
- Negation
- Implication
- Example
- Intuitionistic logic
- Use of prenex form
- References
Every formula in classical logic is equivalent to a formula in prenex normal form. For example, if
is in prenex normal form with matrix
is logically equivalent but not in prenex normal form.
Conversion to prenex form
Every first-order formula is logically equivalent (in classical logic) to some formula in prenex normal form. 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.
Conjunction and disjunction
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. So
Negation
The rules for negation say that
and
Implication
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
The rules for removing quantifiers from the antecedent are:
The rules for removing quantifiers from the consequent are:
Example
Suppose that
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:
Intuitionistic logic
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
is a function which, given a concrete x and a proof of
on the other hand, produces a single concrete value of y and a function that converts any proof of
The rules for converting a formula to prenex form that do fail in intuitionistic logic are:
(1)(x does not appear as a free variable of
Use of prenex form
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.