Aformula of thepredicate calculus is inprenex^[1]normal form (PNF) if it iswritten as a string ofquantifiers andbound variables, called theprefix, followed by a quantifier-free part, called thematrix.^[2] Together with the normal forms inpropositional logic (e.g.disjunctive normal form orconjunctive normal form), it provides acanonical normal form useful inautomated theorem proving.

Every formula inclassical logic islogically equivalent to a formula in prenex normal form. For example, if${\displaystyle \varphi (y)}$,${\displaystyle \psi (z)}$, and${\displaystyle \rho (x)}$ are quantifier-free formulas with the free variables shown then

${\displaystyle \mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(\varphi (y)\vee (\psi (z)\to \rho (x)))}$

is in prenex normal form with matrix${\displaystyle \varphi (y)\vee (\psi (z)\to \rho (x))}$, while

${\displaystyle \mathrm{\forall }x((\mathrm{\exists }y\varphi (y))\vee ((\mathrm{\exists }z\psi (z))\to \rho (x)))}$

is logically equivalent but not in prenex normal form.

This sectionneeds additional citations forverification. Please helpimprove this article byadding citations to reliable sources in this section. Unsourced material may be challenged and removed.(August 2018) (Learn how and when to remove this message)

Everyfirst-order formula islogically 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 whichlogical connectives appear in the formula.

The rules forconjunction anddisjunction say that

${\displaystyle (\mathrm{\forall }x\varphi )\wedge \psi }$ is equivalent to${\displaystyle \mathrm{\forall }x(\varphi \wedge \psi )}$ under (mild) additional condition${\displaystyle \mathrm{\exists }x\mathrm{\top }}$, or, equivalently,${\displaystyle \mathrm{\neg }\mathrm{\forall }x\mathrm{\perp }}$ (meaning that at least one individual exists),

${\displaystyle (\mathrm{\forall }x\varphi )\vee \psi }$ is equivalent to${\displaystyle \mathrm{\forall }x(\varphi \vee \psi )}$;

and

${\displaystyle (\mathrm{\exists }x\varphi )\wedge \psi }$ is equivalent to${\displaystyle \mathrm{\exists }x(\varphi \wedge \psi )}$,

${\displaystyle (\mathrm{\exists }x\varphi )\vee \psi }$ is equivalent to${\displaystyle \mathrm{\exists }x(\varphi \vee \psi )}$ under additional condition${\displaystyle \mathrm{\exists }x\mathrm{\top }}$.

The equivalences are valid when${\displaystyle x}$ does not appear as afree variable of${\displaystyle \psi }$; if${\displaystyle x}$ does appear free in${\displaystyle \psi }$, one can rename the bound${\displaystyle x}$ in${\displaystyle (\mathrm{\exists }x\varphi )}$ and obtain the equivalent${\displaystyle (\mathrm{\exists }{x}^{\prime }\varphi [x/x^{\prime }])}$.

For example, in the language ofrings,

${\displaystyle (\mathrm{\exists }x(x^2=1))\wedge (0=y)}$ is equivalent to${\displaystyle \mathrm{\exists }x(x^2=1\wedge 0=y)}$,

but

${\displaystyle (\mathrm{\exists }x(x^2=1))\wedge (0=x)}$ is not equivalent to${\displaystyle \mathrm{\exists }x(x^2=1\wedge 0=x)}$

because the formula on the left is true in any ring when the free variablex is equal to 0, while the formula on the right has no free variables and is false in any nontrivial ring. So${\displaystyle (\mathrm{\exists }x(x^2=1))\wedge (0=x)}$ will be first rewritten as${\displaystyle (\mathrm{\exists }{x}^{\prime }(x^{\prime 2}=1))\wedge (0=x)}$ and then put in prenex normal form${\displaystyle \mathrm{\exists }{x}^{\prime }(x^{\prime 2}=1\wedge 0=x)}$.

The rules for negation say that

${\displaystyle \mathrm{\neg }\mathrm{\exists }x\varphi }$ is equivalent to${\displaystyle \mathrm{\forall }x\mathrm{\neg }\varphi }$

and

${\displaystyle \mathrm{\neg }\mathrm{\forall }x\varphi }$ is equivalent to${\displaystyle \mathrm{\exists }x\mathrm{\neg }\varphi }$.

There are four rules forimplication: two that remove quantifiers from the antecedent and two that remove quantifiers from the consequent. These rules can be derived byrewriting the implication${\displaystyle \varphi \to \psi }$ as${\displaystyle \mathrm{\neg }\varphi \vee \psi }$ 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):

${\displaystyle (\mathrm{\forall }x\varphi )\to \psi }$ is equivalent to${\displaystyle \mathrm{\exists }x(\varphi \to \psi )}$,

${\displaystyle (\mathrm{\exists }x\varphi )\to \psi }$ is equivalent to${\displaystyle \mathrm{\forall }x(\varphi \to \psi )}$.

The rules for removing quantifiers from the consequent are:

${\displaystyle \varphi \to (\mathrm{\exists }x\psi )}$ is equivalent to${\displaystyle \mathrm{\exists }x(\varphi \to \psi )}$ (under the assumption that${\displaystyle \mathrm{\exists }x\mathrm{\top }}$),

${\displaystyle \varphi \to (\mathrm{\forall }x\psi )}$ is equivalent to${\displaystyle \mathrm{\forall }x(\varphi \to \psi )}$.

For example, when therange of quantification is the non-negativenatural number (viz.${\displaystyle n\in \mathbb{N}}$), the statement

islogically equivalent to the statement

The former statement says that ifx is less than any natural number, thenx is less than zero. The latter statement says that there exists some natural numbern such that ifx is less thann, thenx is less than zero. Both statements are true. The former statement is true because ifx is less than any natural number, it must be less than the smallest natural number (zero). The latter statement is true becausen=0 makes the implication atautology.

Note that the placement of brackets implies thescope of the quantification, which is very important for the meaning of the formula. Consider the following two statements:

and itslogically equivalent statement

The former statement says that for any natural numbern, ifx is less thann thenx is less than zero. The latter statement says that if there exists some natural numbern such thatx is less thann, thenx is less than zero. Both statements are false. The former statement doesn't hold forn=2, becausex=1 is less thann, but not less than zero. The latter statement doesn't hold forx=1, because the natural numbern=2 satisfiesx<n, butx=1 is not less than zero.

Suppose that${\displaystyle \varphi }$,${\displaystyle \psi }$, and${\displaystyle \rho }$ are quantifier-free formulas and no two of these formulas share any free variable. Consider the formula

${\displaystyle (\varphi \vee \mathrm{\exists }x\psi )\to \mathrm{\forall }z\rho }$.

By recursively applying the rules starting at the innermost subformulas, the following sequence of logically equivalent formulas can be obtained:

${\displaystyle (\varphi \vee \mathrm{\exists }x\psi )\to \mathrm{\forall }z\rho }$.

${\displaystyle (\mathrm{\exists }x(\varphi \vee \psi ))\to \mathrm{\forall }z\rho }$,

${\displaystyle \mathrm{\neg }(\mathrm{\exists }x(\varphi \vee \psi ))\vee \mathrm{\forall }z\rho }$,

${\displaystyle (\mathrm{\forall }x\mathrm{\neg }(\varphi \vee \psi ))\vee \mathrm{\forall }z\rho }$,

${\displaystyle \mathrm{\forall }x(\mathrm{\neg }(\varphi \vee \psi )\vee \mathrm{\forall }z\rho )}$,

${\displaystyle \mathrm{\forall }x((\varphi \vee \psi )\to \mathrm{\forall }z\rho )}$,

${\displaystyle \mathrm{\forall }x(\mathrm{\forall }z((\varphi \vee \psi )\to \rho ))}$,

${\displaystyle \mathrm{\forall }x\mathrm{\forall }z((\varphi \vee \psi )\to \rho )}$.

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

${\displaystyle \mathrm{\forall }z\mathrm{\forall }x((\varphi \vee \psi )\to \rho )}$

can be obtained:

${\displaystyle \mathrm{\forall }z((\varphi \vee \mathrm{\exists }x\psi )\to \rho )}$

${\displaystyle \mathrm{\forall }z((\mathrm{\exists }x(\varphi \vee \psi ))\to \rho )}$,

${\displaystyle \mathrm{\forall }z(\mathrm{\forall }x((\varphi \vee \psi )\to \rho ))}$,

${\displaystyle \mathrm{\forall }z\mathrm{\forall }x((\varphi \vee \psi )\to \rho )}$.

Theordering 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. Inintuitionistic 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.

TheBHK interpretation illustrates why some formulas have no intuitionistically-equivalent prenex form. In this interpretation, a proof of

${\displaystyle (\mathrm{\exists }x\varphi )\to \mathrm{\exists }y\psi (1)}$

is a function which, given a concretex and a proof of${\displaystyle \varphi (x)}$, produces a concretey and a proof of${\displaystyle \psi (y)}$. In this case it is allowable for the value ofy to be computed from the given value ofx. A proof of

${\displaystyle \mathrm{\exists }y(\mathrm{\exists }x\varphi \to \psi ),(2)}$

on the other hand, produces a single concrete value ofy and a function that converts any proof of${\displaystyle \mathrm{\exists }x\varphi }$ into a proof of${\displaystyle \psi (y)}$. If eachx satisfying${\displaystyle \varphi }$ can be used to construct ay satisfying${\displaystyle \psi }$ but no suchy can be constructed without knowledge of such anx then formula (1) will not be equivalent to formula (2).

The rules for converting a formula to prenex form that dofail in intuitionistic logic are:

(1)${\displaystyle \mathrm{\forall }x(\varphi \vee \psi )}$ implies${\displaystyle (\mathrm{\forall }x\varphi )\vee \psi }$,

(2)${\displaystyle \mathrm{\forall }x(\varphi \vee \psi )}$ implies${\displaystyle \varphi \vee (\mathrm{\forall }x\psi )}$,

(3)${\displaystyle (\mathrm{\forall }x\varphi )\to \psi }$ implies${\displaystyle \mathrm{\exists }x(\varphi \to \psi )}$,

(4)${\displaystyle \varphi \to (\mathrm{\exists }x\psi )}$ implies${\displaystyle \mathrm{\exists }x(\varphi \to \psi )}$,

(5)${\displaystyle \mathrm{\neg }\mathrm{\forall }x\varphi }$ implies${\displaystyle \mathrm{\exists }x\mathrm{\neg }\varphi }$,

(x does not appear as a free variable of${\displaystyle \psi }$ in (1) and (3);x does not appear as a free variable of${\displaystyle \varphi }$ in (2) and (4)).

Someproof calculi will only deal with a theory whose formulae are written in prenex normal form. The concept is essential for developing thearithmetical hierarchy and theanalytical hierarchy.

Gödel's proof of hiscompleteness theorem forfirst-order logic presupposes that all formulae have been recast in prenex normal form.

Tarski's axioms for geometry is a logical system whose sentences canall be written inuniversal–existential form, a special case of the prenex normal form that has everyuniversal quantifier preceding anyexistential quantifier, so that all sentences can be rewritten in the form${\displaystyle \mathrm{\forall }u}$ ${\displaystyle \mathrm{\forall }v}$ ${\displaystyle \dots }$ ${\displaystyle \mathrm{\exists }a}$ ${\displaystyle \mathrm{\exists }b}$ ${\displaystyle \varphi }$, where${\displaystyle \varphi }$ is a sentence that does not contain any quantifier. This fact allowedTarski to prove that Euclidean geometry isdecidable.

Look upprenex in Wiktionary, the free dictionary.

• Arithmetical hierarchy
• Herbrandization
• Skolemization

• Richard L. Epstein (18 December 2011).Classical Mathematical Logic: The Semantic Foundations of Logic. Princeton University Press. pp. 108–.ISBN 978-1-4008-4155-4.
• Peter B. Andrews (17 April 2013).An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Springer Science & Business Media. pp. 111–.ISBN 978-94-015-9934-4.
• Elliott Mendelson (1 June 1997).Introduction to Mathematical Logic, Fourth Edition. CRC Press. pp. 109–.ISBN 978-0-412-80830-2.
• Hinman, Peter (2005),Fundamentals of Mathematical Logic,A K Peters,ISBN 978-1-56881-262-5

• Normal forms (logic)

• Articles with short description
• Short description is different from Wikidata
• Articles needing additional references from August 2018
• All articles needing additional references