Editing Prenex normal form

{{Short description|Formalism of first-order logic}}
A [[formula (mathematical logic)|formula]] of the [[predicate calculus]] is in '''prenex<ref>The term 'prenex' comes from the [[Latin]] ''praenexus'' "tied or bound up in front", past participle of ''praenectere'' [http://cs.nyu.edu/pipermail/fom/2007-November/012328.html] (archived as of May 27, 2011 at [https://web.archive.org/web/20110527102347/http://cs.nyu.edu/pipermail/fom/2007-November/012328.html])</ref> [[Normal form (abstract rewriting)|normal form]]''' ('''PNF''') if it is [[Rewriting#Logic|written]] as a string of [[quantifier (logic)|quantifiers]] and [[bound variable|bound variables]], called the '''prefix''', followed by a quantifier-free part, called the '''matrix'''.<ref>Hinman, P. (2005), p. 110</ref> Together with the normal forms in [[Propositional calculus|propositional logic]] (e.g. [[disjunctive normal form]] or [[conjunctive normal form]]), it provides a [[canonical normal form]] useful in [[automated theorem proving]]. 

Every formula in [[classical logic]] is [[logically equivalent]] to a formula in prenex normal form. For example, if <math>\phi(y)</math>, <math>\psi(z)</math>, and <math>\rho(x)</math> are quantifier-free formulas with the free variables shown then
:<math>\forall x \exists y \forall z (\phi(y) \lor (\psi(z) \rightarrow \rho(x)))</math>
is in prenex normal form with matrix <math>\phi(y) \lor (\psi(z) \rightarrow \rho(x))</math>, while
:<math>\forall x ((\exists y \phi(y)) \lor ((\exists z \psi(z) ) \rightarrow \rho(x)))</math>
is logically equivalent but not in prenex normal form.

== Conversion to prenex form ==
{{refimprove section|date=August 2018}}
Every [[first-order predicate calculus|first-order]] formula is [[logically equivalent]] (in classical logic) to some formula in prenex normal form.<ref>Hinman, P. (2005), p. 111</ref>  There are several conversion rules that can be recursively applied to convert a formula to prenex normal form.  The rules depend on which [[logical connective]]s appear in the formula. 

=== Conjunction and disjunction ===

The rules for [[logical conjunction|conjunction]] and [[logical disjunction|disjunction]] say that
:<math>(\forall x \phi) \land \psi</math> is equivalent to <math>\forall x ( \phi \land \psi)</math> under (mild) additional condition <math>\exists x \top</math>, or, equivalently, <math>\lnot\forall x \bot</math> (meaning that at least one individual exists),
:<math>(\forall x \phi) \lor \psi</math> is equivalent to <math>\forall x ( \phi \lor \psi)</math>;
and 
:<math>(\exists x \phi) \land \psi</math> is equivalent to <math>\exists x (\phi \land \psi)</math>,
:<math>(\exists x \phi) \lor \psi</math> is equivalent to <math>\exists x (\phi \lor \psi)</math> under additional condition <math>\exists x \top</math>.
The equivalences are valid when <math>x</math> does not appear as a [[free variable]] of <math>\psi</math>; if <math>x</math> does appear free in <math>\psi</math>, one can rename the bound <math>x</math> in <math>(\exists x \phi)</math> and obtain the equivalent <math>(\exists x' \phi[x/x'])</math>.

For example, in the language of [[ring (mathematics)|rings]],
:<math>(\exists x (x^2 = 1)) \land (0 = y)</math> is equivalent to  <math>\exists x ( x^2 = 1 \land 0 = y)</math>,
but
:<math>(\exists x (x^2 = 1)) \land (0 = x)</math> is not equivalent to <math>\exists x ( x^2 = 1 \land 0 = x)</math>
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 <math>(\exists x (x^2 = 1)) \land (0 = x)</math> will be first rewritten as <math>(\exists x' (x'^2 = 1)) \land (0 = x)</math> and then put in prenex normal form <math>\exists x' ( x'^2 = 1 \land 0 = x)</math>.

=== Negation ===

The rules for negation say that 
:<math>\lnot \exists x \phi</math> is equivalent to <math>\forall x \lnot \phi</math> 
and 
:<math>\lnot \forall x \phi</math> is equivalent to <math>\exists x \lnot \phi</math>.

=== Implication ===

There are four rules for [[material conditional|implication]]: two that remove quantifiers from the antecedent and two that remove quantifiers from the consequent. These rules can be derived by [[Rewriting#Logic|rewriting]] the implication
<math>\phi \rightarrow \psi</math> as <math>\lnot \phi \lor \psi</math> 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):
:<math>(\forall x \phi ) \rightarrow \psi</math> is equivalent to <math>\exists x (\phi \rightarrow \psi)</math> (under the assumption that <math>\exists x \top</math>),
:<math>(\exists x \phi ) \rightarrow \psi</math> is equivalent to <math>\forall x (\phi \rightarrow \psi)</math>.
The rules for removing quantifiers from the consequent are:
:<math>\phi \rightarrow (\exists x \psi)</math> is equivalent to <math>\exists x (\phi \rightarrow \psi)</math> (under the assumption that <math>\exists x \top</math>),
:<math>\phi \rightarrow (\forall x \psi)</math> is equivalent to <math>\forall x (\phi \rightarrow \psi)</math>.
For example, when the [[range of quantification]] is the non-negative [[natural number]] (viz. <math>n\in \mathbb{N}</math>), the statement
:<math>[\forall n\in \mathbb{N} (x< n) ] \rightarrow (x< 0)</math>
is [[logically equivalent]] to the statement
:<math>\exists n\in \mathbb{N}[ (x< n)  \rightarrow (x< 0)]</math>
The former statement says that if ''x'' is less than any natural number, then ''x'' is less than zero. 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. Both statements are true. The former statement is true because if ''x'' is less than any natural number, it must be less than the smallest natural number (zero). The latter statement is true because ''n=0'' makes the implication a [[Tautology (logic)|tautology]].

Note that the placement of brackets implies the [[Scope (logic)|scope of the quantification]], which is very important for the meaning of the formula. Consider the following two statements:
:<math>\forall n\in \mathbb{N} [(x< n) \rightarrow (x< 0)]</math>
and its [[logically equivalent]] statement
:<math>[\exists n\in \mathbb{N} (x< n) ] \rightarrow (x< 0)</math>
The former statement says that for any natural number ''n'', if ''x'' is less than ''n'' then ''x'' is less than zero. 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. Both statements are false. The former statement doesn't hold for ''n=2'', because ''x=1'' is less than ''n'', but not less than zero. The latter statement doesn't hold for ''x=1'', because the natural number ''n=2'' satisfies ''x<n'', but ''x=1'' is not less than zero.

=== Example ===

Suppose that <math>\phi</math>, <math>\psi</math>, and <math>\rho</math> are quantifier-free formulas and no two of these formulas share any free variable.   Consider the formula
:<math> (\phi \lor \exists x \psi) \rightarrow \forall z \rho</math>.
By recursively applying the rules starting at the innermost subformulas, the following sequence of logically equivalent formulas can be obtained:
:<math> (\phi \lor \exists x \psi) \rightarrow \forall z \rho</math>.
:<math> ( \exists x (\phi \lor \psi) ) \rightarrow \forall z \rho</math>,
:<math> \neg( \exists x (\phi \lor \psi) ) \lor \forall z \rho</math>,
:<math> (\forall x \neg(\phi \lor \psi)) \lor \forall z \rho</math>,
:<math> \forall x (\neg(\phi \lor \psi) \lor \forall z \rho)</math>,
:<math> \forall x ( ( \phi \lor \psi) \rightarrow \forall z \rho )</math>,
:<math> \forall x ( \forall z (( \phi \lor \psi) \rightarrow \rho ))</math>,
:<math> \forall x \forall z ( ( \phi \lor \psi) \rightarrow \rho )</math>.
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
:<math>\forall z \forall x ( ( \phi \lor \psi) \rightarrow \rho)</math>
can be obtained: 
:<math> \forall z (  (\phi \lor \exists x \psi) \rightarrow \rho )</math>
:<math> \forall z (  (\exists x (\phi \lor \psi) ) \rightarrow \rho )</math>,
:<math> \forall z (  \forall x ( (\phi \lor \psi) \rightarrow \rho ) )</math>,
:<math> \forall z \forall x ( (\phi \lor \psi) \rightarrow \rho )</math>.
The [[Quantifier (logic)#Order of quantifiers (nesting)|ordering]] of the two universal quantifier with the same scope doesn't change the meaning/truth value of the statement.

=== 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 
:<math>(\exists x \phi) \rightarrow \exists y \psi \qquad (1)</math>
is a function which, given a concrete ''x'' and a proof of <math>\phi (x)</math>, produces a concrete ''y'' and a proof of <math>\psi (y)</math>.  In this case it is allowable for the value of ''y'' to be computed from the given value of ''x''.  A proof of 
:<math>\exists y ( \exists x \phi \rightarrow \psi), \qquad  (2)</math>
on the other hand, produces a single concrete value of ''y'' and a function that converts any proof of <math>\exists x \phi</math> into a proof of <math>\psi (y)</math>.   If each ''x''  satisfying <math>\phi</math> can be used to construct a ''y'' satisfying <math>\psi</math> 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) <math>\forall x (\phi \lor \psi)</math> implies <math>(\forall x \phi) \lor \psi</math>,
:(2) <math>\forall x (\phi \lor \psi)</math> implies <math>\phi \lor (\forall x \psi)</math>,
:(3) <math>(\forall x \phi) \rightarrow \psi</math> implies <math>\exists x (\phi \rightarrow \psi)</math>,
:(4) <math>\phi \rightarrow (\exists x \psi)</math> implies <math>\exists x (\phi \rightarrow \psi)</math>,
:(5) <math>\lnot \forall x \phi</math> implies <math>\exists x \lnot \phi</math>,
(''x'' does not appear as a free variable of <math>\,\psi</math> in (1) and (3); ''x'' does not appear as a free variable of <math>\,\phi</math> in (2) and (4)).

== Use of prenex form ==

Some [[proof calculus|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 [[Gödel's completeness theorem|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 quantification|universal quantifier]] preceding any [[existential quantification|existential quantifier]], so that all sentences can be rewritten in the form <math>\forall u</math>&nbsp;<math>\forall v</math>&nbsp;<math>\ldots</math>&nbsp;<math>\exists a</math>&nbsp;<math>\exists b</math>&nbsp;<math>\phi</math>, where <math>\phi</math> is a sentence that does not contain any quantifier. This fact allowed [[Alfred Tarski|Tarski]] to prove that Euclidean geometry is [[decidability (logic)|decidable]].

==See also==
{{Wiktionary|prenex}}
*[[Arithmetical hierarchy]]
*[[Herbrandization]]
*[[Skolemization]]

==Notes==
{{reflist}}

==References==
* {{cite book|author=Richard L. Epstein|title=Classical Mathematical Logic: The Semantic Foundations of Logic|url=https://books.google.com/books?id=-7HpkQRvQhoC&q=%22prenex+normal+form%22&pg=PA108|date=18 December 2011|publisher=Princeton University Press|isbn=978-1-4008-4155-4|pages=108–}}
* {{cite book|author=[[Peter B. Andrews]]|title=An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof|url=https://books.google.com/books?id=UaPuCAAAQBAJ&q=%22prenex+normal+form%22&pg=PA111|date=17 April 2013|publisher=Springer Science & Business Media|isbn=978-94-015-9934-4|pages=111–}}
* {{cite book|author=[[Elliott Mendelson]]|title=Introduction to Mathematical Logic, Fourth Edition|url=https://books.google.com/books?id=ZO1p4QGspoYC&q=%22prenex+normal+form%22&pg=PA109|date=1 June 1997|publisher=CRC Press|isbn=978-0-412-80830-2|pages=109–}}
* {{Citation | last1=Hinman | first1=Peter | title=Fundamentals of Mathematical Logic | publisher=[[A K Peters]] | isbn=978-1-56881-262-5 | year=2005}}

[[Category:Normal forms (logic)]]
{{Normal forms in logic}}