Prenex formula

A formula from the restricted predicate calculus having the form

where denotes the universal quantifier or the existential quantifier , the variables are distinct for , and is a formula without quantifiers. Prenex formulas are also called prenex normal forms or prenex forms.

For each formula of the language of the restricted predicate calculus there is a prenex formula that is logically equivalent to 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:

where is any variable not appearing as a free variable in or , and can be obtained from by changing all free appearances of to ; the variable does not appear as a free variable in or . To use the above equivalences one has to first express all logical operators by and 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