A formula of the predicate calculus is in prenex normal form 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 , 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 ϕ {\displaystyle \phi } , ψ {\displaystyle \psi } , and ρ {\displaystyle \rho } are quantifier-free formulas with the free variables shown then
is in prenex normal form with matrix ϕ ∨ → ρ ] {\displaystyle \phi \lor \rightarrow \rho ]} , while
is logically equivalent but not in prenex normal form.