In predicate logic, a well-formed formula is in prenex normal form (PNF) if it has all of its quantifiers in fronts. For example,
is in the prenex normal form, while
is logically equivalent but not in the prenex normal form.
We can convert a formula into the prenex normal form by moving quantifiers.