 Prenex normal form

A formula of the predicate calculus is in prenex^{[1]} normal form if it is written as a string of quantifiers followed by a quantifierfree part (referred to as the matrix).
Every formula in classical logic is equivalent to a formula in prenex normal form. For example, if φ(y), ψ(z), and ρ(x) are quantifierfree formulas with the free variables shown then
is in prenex normal form with matrix , while
is logically equivalent but not in prenex normal form.
Contents
Conversion to prenex form
Every firstorder 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
 is equivalent to ,
 is equivalent to ;
and
 is equivalent to ,
 is equivalent to .
The equivalences are valid when x does not appear as a free variable of ψ; if x does appear free in ψ, it must be replaced with another free variable.
For example, in the language of rings,
 is equivalent to ,
but
 is not equivalent to
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.
Negation
The rules for negation say that
 is equivalent to
and
 is equivalent to .
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 as and applying the rules for disjunction 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:
 is equivalent to ,
 is equivalent to .
The rules for removing quantifiers from the consequent are:
 is equivalent to ,
 is equivalent to .
Example
Suppose that ϕ, ψ, and ρ are quantifierfree formulas and no two of these formulas share any free variable. 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:
 ,
 ,
 .
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 intuitionisticallyequivalent prenex form. In this interpretation, a proof of
is a function which, given a concrete x and a proof of φ(x), produces a concrete y and a proof of ψ(y). In this case it is allowable for the value of y to be computed from the given value of x. A proof of
on the other hand, produces a single concrete value of y and a function that converts any proof of into a proof of ψ(y). If each x satisfying φ can be used to construct a y satisfying ψ but no such y can be constructed without knowledge of such an x then formula (1) will not be equivalent to formula (2).
The rules for converting a formula to prenex form that do fail in intuitionistic logic are:
 (1) implies ,
 (2) implies ,
 (3) implies ,
 (4) implies ,
 (5) implies ,
(x does not appear as a free variable of in (1) and (3); x does not appear as a free variable of in (2) and (4)).
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 firstorder logic presupposes that all formulae have been recast in prenex normal form.
See also
 Herbrandization
 Skolemization
 Arithmetical hierarchy
Notes
References
 Hinman, P. (2005), Fundamentals of Mathematical Logic, A K Peters, ISBN 9781568812625
Categories: Normal forms (logic)
Wikimedia Foundation. 2010.
Look at other dictionaries:
prenex normal form — A well formed formula of the predicate calculus is in prenex normal form if all the quantifiers stand at the front, and any other logical constant stands within the scope of all the quantifiers … Philosophy dictionary
prenex normal form — ˈprēˌneks noun Etymology: Late Latin praenexus tied up or bound in front, from Latin prae pre + nexus, past participle of nectere to tie, bind more at annex : a normal form of an expression in the functional calculus in which all the quantifiers… … Useful english dictionary
Normal form — may refer to: Normal form (abstract rewriting) Normal form (databases) Normal form (game theory) Normal form (mathematics) In formal language theory: Beta normal form Chomsky normal form Greibach normal form Kuroda normal form Normal form… … Wikipedia
Skolem normal form — A formula of first order logic is in Skolem normal form (named after Thoralf Skolem) if it is in conjunctive prenex normal form with only universal first order quantifiers. Every first order formula can be converted into Skolem normal form while… … Wikipedia
Skolem normal form — A formula is in Skolem normal form if it is in prenex normal form, and all the existential quantifiers come first. There is an effective procedure producing, for any formula, one in Skolem normal form that is valid if and only if the original is… … Philosophy dictionary
Canonical form — Generally, in mathematics, a canonical form (often called normal form or standard form) of an object is a standard way of presenting that object. Canonical form can also mean a differential form that is defined in a natural (canonical) way; see… … Wikipedia
True quantified Boolean formula — The language TQBF is a formal language in computer science that contains True Quantified Boolean Formulas. A fully quantified boolean formula is a formula in first order logic where every variable is quantified (or bound), using either… … Wikipedia
metalogic — /met euh loj ik/, n. the logical analysis of the fundamental concepts of logic. [1835 45; META + LOGIC] * * * Study of the syntax and the semantics of formal languages and formal systems. It is related to, but does not include, the formal… … Universalium
Firstorder logic — is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic (a less… … Wikipedia
Rules of passage (logic) — In mathematical logic, the rules of passage govern how quantifiers distribute over the basic logical connectives of first order logic. The rules of passage govern the passage (translation) from any formula of first order logic to the equivalent… … Wikipedia