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.

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