View source for Prenex formula

A formula from the [[Restricted predicate calculus|restricted predicate calculus]] having the form

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p0744201.png" /></td> </tr></table>

where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p0744202.png" /> denotes the [[Universal quantifier|universal quantifier]] <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p0744203.png" /> or the [[Existential quantifier|existential quantifier]] <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p0744204.png" />, the variables <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p0744205.png" /> are distinct for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p0744206.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p0744207.png" /> is a formula without quantifiers. Prenex formulas are also called prenex normal forms or prenex forms.

For each formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p0744208.png" /> of the language of the restricted predicate calculus there is a prenex formula that is logically equivalent to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p0744209.png" /> in the classical [[Predicate calculus|predicate calculus]]. The procedure of finding a prenex formula is based on the following equivalences, which can be deduced in the classical predicate calculus:

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442010.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442011.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442012.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442013.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442014.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442015.png" /></td> </tr></table>

where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442016.png" /> is any variable not appearing as a free variable in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442017.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442018.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442019.png" /> can be obtained from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442020.png" /> by changing all free appearances of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442021.png" /> to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442022.png" />; the variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442023.png" /> does not appear as a free variable in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442024.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442025.png" />. To use the above equivalences one has to first express all logical operators by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442026.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074420/p07442027.png" /> 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====
<table><TR><TD valign="top">[1]</TD> <TD valign="top"> E. Mendelson, "Introduction to mathematical logic" , v. Nostrand (1964) {{MR|0164867}} {{ZBL|1173.03001}} {{ZBL|0915.03002}} {{ZBL|0681.03001}} {{ZBL|0534.03001}} {{ZBL|0498.03001}} {{ZBL|0192.01901}} </TD></TR></table>



====Comments====


====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top"> S.C. Kleene, "Introduction to metamathematics" , North-Holland (1950) pp. Chapt. VII, §35 {{MR|1234051}} {{MR|1570642}} {{MR|0051790}} {{ZBL|0875.03002}} {{ZBL|0604.03002}} {{ZBL|0109.00509}} {{ZBL|0047.00703}} </TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top"> R. Fraissé, "Course of mathematical logic" , '''1''' , Reidel (1973) pp. Sect. 5.1.1ff {{MR|0345784}} {{ZBL|0262.02001}} </TD></TR></table>