Prenex

Prenex is a term used in logic to describe a standard form of a first-order logic formula, known as prenex normal form. A formula is in prenex normal form if all quantifiers appear at the front, followed by a quantifier-free core called the matrix. The prefix at the front is a sequence of universal and existential quantifiers, for example ∀x ∃y. The matrix contains no quantifiers and uses the remaining free variables.

The idea behind prenex normal form is to separate the binding structure of the quantifiers from the logical content of the formula. Any classical first-order formula can be transformed into an equivalent formula in prenex normal form by removing implications and biconditionals, pushing negations inward (via De Morgan’s laws and quantifier negation rules), standardizing bound variables to avoid capture, and then moving all quantifiers to the front using standard equivalences. The result is a prefix of quantifiers followed by a quantifier-free matrix. Note that the order of universal and existential quantifiers in the prefix generally matters for equivalence, and the process may introduce many renamings of bound variables.

Example: the formula ∀x (P(x) → ∃y Q(x,y)) can be rewritten as ∀x ∃y (¬P(x) ∨ Q(x,y)), which is in prenex form with the prefix ∀x ∃y and the quantifier-free matrix ¬P(x) ∨ Q(x,y).

Applications of prenex normal form appear in proof theory, automated theorem proving, and model checking. It is often followed by Skolemization to obtain a form suitable for resolution, where existential quantifiers are eliminated by introducing new function symbols.