Бірінші реттік логикадағы пренекс нормалық форма

Formalism of first order logic
A formula of the predicate calculus is in prenex normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier free part, called the matrix. Together with the normal forms in propositional logic (e. g. disjunctive normal form or conjunctive normal form), it provides a canonical normal form useful in automated theorem proving. Every formula in classical logic is logically equivalent to a formula in prenex normal form. For example, if , , and are quantifier free formulas with the free variables shown then

is in prenex normal form with matrix , while

is logically equivalent but not in prenex normal form.

Every first order formula is logically equivalent (in classical logic) to some formula in prenex normal form. There are several conversion rules that can be recursively applied to convert a formula to prenex normal form. The rules depend on which logical connectives appear in the formula.

Some 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 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 quantifier preceding any existential quantifier, so that all sentences can be rewritten in the form      , where is a sentence that does not contain any quantifier. This fact allowed Tarski to prove that Euclidean geometry is decidable.