Prenex normal form
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).
Every formula in classical logic
is equivalent to a formula in prenex normal form. For example, if
, 
, and 
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.
s appear in the formula.
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.
is equivalent to 
and
is equivalent to 
.
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 
.
, 
, and 
are quantifier-free 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:
,
,
.
, 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 φ(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:
implies 
, 
implies 
, 
implies 
, 
implies 
, 
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)).
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.
Normal form
Normal form may refer to:* Normal form * Normal form * Normal form * Normal form In formal language theory:* Beta normal form* Chomsky normal form* Greibach normal form* Kuroda normal form...
if it is written as a string of quantifiers followed by a quantifier-free part (referred to as the matrix).
Every formula in classical logic
Classical logic
Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...
is equivalent to a formula in prenex normal form. For example, if
, , and are quantifier-free formulas with the free variables shown thenis in prenex normal form with matrix
, whileis 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 connectiveLogical connective
In logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...
s 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
Ring (mathematics)
In mathematics, a ring is an algebraic structure consisting of a set together with two binary operations usually called addition and multiplication, where the set is an abelian group under addition and a semigroup under multiplication such that multiplication distributes over addition...
,
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 quantifier-free 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 logicIntuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
, 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
BHK interpretation
In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer, Arend Heyting and independently by Andrey Kolmogorov...
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 φ(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:
implies , implies , implies , implies , 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 calculiProof calculus
In mathematical logic, a proof calculus corresponds to a family of formal systems that use a common style of formal inference for its inference rules...
will only deal with a theory whose formulae are written in prenex normal form. The concept is essential for developing the arithmetical hierarchy
Arithmetical hierarchy
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene-Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them...
and the analytical hierarchy
Analytical hierarchy
In mathematical logic and descriptive set theory, the analytical hierarchy is a higher type analogue of the arithmetical hierarchy. It thus continues the classification of sets by the formulas that define them.-The analytical hierarchy of formulas:...
.
Gödel
Godel
Godel or similar can mean:*Kurt Gödel , an Austrian logician, mathematician and philosopher*Gödel...
's proof of his completeness theorem
Gödel's completeness theorem
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....
for first-order logic
First-order logic
First-order 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...
presupposes that all formulae have been recast in prenex normal form.