Prenex normal form

A formula of the predicate calculus is in prenex^[1] 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.^[2] 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 ${\displaystyle \phi (y)}$, ${\displaystyle \psi (z)}$, and ${\displaystyle \rho (x)}$ are quantifier-free formulas with the free variables shown then

${\displaystyle \forall x\exists y\forall z(\phi (y)\lor (\psi (z)\rightarrow \rho (x)))}$

is in prenex normal form with matrix ${\displaystyle \phi (y)\lor (\psi (z)\rightarrow \rho (x))}$, while

${\displaystyle \forall x((\exists y\phi (y))\lor ((\exists z\psi (z))\rightarrow \rho (x)))}$

is logically equivalent but not in prenex normal form.