Prenex normal form
A formula of the predicate calculus is in prenex normal form (PNF) if it is rewritten 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 equivalent to a formula in prenex normal form. For example, if formula_1, formula_2, and formula_3 are quantifier-free formulas with the free variables shown then is in prenex  normal form with matrix formula_5, while is logically equivalent but not in prenex normal form. Conversion to prenex 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. Conjunction and disjunction. The rules for conjunction and disjunction say that and The equivalences are valid when formula_18 does not appear as a free variable of formula_19; if formula_18 does appear free in formula_19, one  can rename the bound formula_18 in formula_23 and obtain the equivalent formula_24. For example, in the language of rings, but because the formula on the left is true in any ring when the free variable "x" is equal to 0, while the formula on the right has no free variables and is false in any nontrivial ring. So formula_27 will be first rewritten as formula_30 and then put in prenex normal form formula_31. Negation. The rules for negation say that and Implication. There are four rules for implication: two that remove quantifiers from the antecedent and two that remove quantifiers  from the consequent. These rules can be derived by rewriting the implication formula_36 as formula_37 and applying the rules for disjunction above. As with the rules for disjunction, these rules require that the variable quantified in one subformula does not appear free in the other subformula. The rules for removing quantifiers from the antecedent are (note the change of quantifiers): The rules for removing quantifiers from the consequent are: For example, when the range of quantification is the non-negative natural number (viz. formula_48), the statement is logically equivalent to the statement The former statement says that if "x" is  less than any natural number, then "x" is less than zero; The latter statement says that there exists some natural number "n" such that if "x" is less than "n", then "x" is less than zero. Both statements are true. The former statement is true because if "x" is less than any natural number, it must be less than the smallest natural number (zero); The latter is true because "n=0" makes the implication a tautology. Note that the placement of brackets implies the scope of the quantification, which is very important for the meaning of the formula. Consider the following  two statements: and its logically equivalent statement The former statement says that for any natural number "n", if "x" is less than "n" then "x" is less than zero; The latter statement says that if there exists some natural number "n" such that "x" is less than "n", then "x" is less than zero. Both statements are false. The former statement doesn't hold for "n=2", because "x=1" is less than "n", but not less than zero; The latter doesn't hold for "x=1", because the natural number "n=2" satisfies "x<n", but "x=1" is not less than zero . Example. Suppose that formula_53, formula_19, and formula_55 are quantifier-free formulas and no two of these formulas share any free variable. Consider the formula By recursively applying the rules starting at the innermost subformulas, the following sequence of logically equivalent formulas can be obtained: This is not the only prenex form equivalent to the original formula. For example, by dealing with the consequent before the antecedent in the example above, the prenex form can be obtained: The ordering of the two universal quantifier with the same scope doesn't change the meaning/truth value of the statement. Intuitionistic logic. The  rules for converting a formula to prenex form make heavy use of classical logic. In intuitionistic logic, it is not true that every formula is logically equivalent to a prenex formula. The negation connective is one obstacle, but not the only one. The implication operator is also treated differently in intuitionistic logic than classical logic; in intuitionistic logic, it is not definable using disjunction and negation. The BHK interpretation illustrates why some formulas have no intuitionistically-equivalent prenex form. In this interpretation, a proof of is a function which, given a concrete "x" and a proof of formula_71, produces a  concrete "y" and a proof of formula_72. In this case it is allowable for the value of "y" to be computed from the given value of "x". A proof of on the other hand, produces a single concrete value of "y" and a function that converts any proof of formula_74 into a proof of formula_72. If each "x" satisfying formula_53 can be used to construct a "y" satisfying formula_19 but no such "y" can be constructed without knowledge of such an "x" then formula (1) will not be equivalent to formula (2). The rules for converting a formula to prenex  form that do "fail" in intuitionistic logic are: ("x" does not appear as a free variable of formula_88 in (1) and (3); "x" does not appear as a free variable of formula_89 in (2) and (4)). Use of prenex form. 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 formula_90 formula_91 formula_92 formula_93 formula_94 formula_53, where formula_53 is a sentence that does not contain any quantifier. This fact allowed Tarski to prove that Euclidean geometry is decidable.