# Prenex formula

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.

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