What is "prenex normal form"

n. (context logic English) A way of expressing a formula of predicate logic such the formula consists of a prenex and a matrix, with the prenex preceding the matrix.

A formula of the predicate calculus is in prenex normal form if it is written as a string of quantifiers (referred to as the prefix) followed by a quantifier-free part (referred to as the matrix).

Every formula in classical logic is equivalent to a formula in prenex normal form. For example, if ϕ(y), ψ(z), and ρ(x) are quantifier-free formulas with the free variables shown then

∀x∃y∀z(ϕ(y) ∨ (ψ(z) → ρ(x)))
is in prenex normal form with matrix ϕ(y) ∨ (ψ(z) → ρ(x)), while

∀x((∃yϕ(y)) ∨ ((∃zψ(z)) → ρ(x)))
is logically equivalent but not in prenex normal form.