# Prenex formula

Jump to: navigation, search

A formula from the restricted predicate calculus having the form

$$Q _ {1} x _ {1} \dots Q _ {n} x _ {n} \Psi ,$$

where $Q _ {i}$ denotes the universal quantifier $\forall$ or the existential quantifier $\exists$, the variables $x _ {i} , x _ {j}$ are distinct for $i \neq j$, and $\psi$ is a formula without quantifiers. Prenex formulas are also called prenex normal forms or prenex forms.

For each formula $\phi$ of the language of the restricted predicate calculus there is a prenex formula that is logically equivalent to $\phi$ in the classical predicate calculus. The procedure of finding a prenex formula is based on the following equivalences, which can be deduced in the classical predicate calculus:

$$( \forall x \phi ( x) \supset \Psi ) \equiv \ \exists x ^ \prime ( \phi ( x ^ \prime ) \supset \Psi ) ,$$

$$\exists x \phi ( x) \supset \Psi \equiv \ \forall x ^ \prime ( \phi ( x ^ \prime ) \supset \Psi ) ,$$

$$\Psi \supset \forall x \phi ( x) \equiv \ \forall x ^ \prime ( \Psi \supset \phi ( x ^ \prime ) ) ,$$

$$\Psi \supset \exists x \phi ( x) \equiv \ \exists x ^ \prime ( \Psi \supset \phi ( x ^ \prime ) ) ,$$

$$\neg \forall x \phi \equiv \exists x \neg \phi ,\ \ \neg \exists x \phi \equiv \forall x \neg \phi ,$$

$$Q y \forall x \phi \equiv \forall x \phi ,\ Q y \exists x \phi \equiv \exists x \phi ,$$

where $x ^ \prime$ is any variable not appearing as a free variable in $\phi ( x)$ or $\psi$, and $\phi ( x ^ \prime )$ can be obtained from $\phi ( x)$ by changing all free appearances of $x$ to $x ^ \prime$; the variable $y$ does not appear as a free variable in $\forall x \phi$ or $\exists x \phi$. To use the above equivalences one has to first express all logical operators by $\supset$ and $\neg$ and then move all quantifiers to the left by applying the equivalences. The prenex formula thus obtained is called the prenex form of the given formula.

#### References

 [1] E. Mendelson, "Introduction to mathematical logic" , v. Nostrand (1964) MR0164867 Zbl 1173.03001 Zbl 0915.03002 Zbl 0681.03001 Zbl 0534.03001 Zbl 0498.03001 Zbl 0192.01901

#### References

 [a1] S.C. Kleene, "Introduction to metamathematics" , North-Holland (1950) pp. Chapt. VII, §35 MR1234051 MR1570642 MR0051790 Zbl 0875.03002 Zbl 0604.03002 Zbl 0109.00509 Zbl 0047.00703 [a2] R. Fraissé, "Course of mathematical logic" , 1 , Reidel (1973) pp. Sect. 5.1.1ff MR0345784 Zbl 0262.02001
How to Cite This Entry:
Prenex formula. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Prenex_formula&oldid=48280
This article was adapted from an original article by V.N. Grishin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article