Editing Prenex normal form (section)

== Use of prenex form ==

Some [[proof calculus|proof calculi]] will only deal with a theory whose formulae are written in prenex normal form. The concept is essential for developing the [[arithmetical hierarchy]] and the [[analytical hierarchy]].

[[Gödel]]'s proof of his [[Gödel's completeness theorem|completeness theorem]] for [[first-order logic]] presupposes that all formulae have been recast in prenex normal form.

[[Tarski's axioms]] for geometry is a logical system whose sentences can ''all'' be written in '''universal–existential form''', a special case of the prenex normal form that has every [[universal quantification|universal quantifier]] preceding any [[existential quantification|existential quantifier]], so that all sentences can be rewritten in the form <math>\forall u</math>&nbsp;<math>\forall v</math>&nbsp;<math>\ldots</math>&nbsp;<math>\exists a</math>&nbsp;<math>\exists b</math>&nbsp;<math>\phi</math>, where <math>\phi</math> is a sentence that does not contain any quantifier. This fact allowed [[Alfred Tarski|Tarski]] to prove that Euclidean geometry is [[decidability (logic)|decidable]].