Prenex Normal Form

A formula of first-order logic is in prenex normal form if it is of the form


where each Q_i is a quantifier  forall ("for all") or  exists ("exists") and M is quantifier-free.

For example, the formula

  exists x forall y exists z(P(x) v Q(x,y,z))

is in prenex normal form, whereas formula

  exists x forall y(P(x) v  exists zQ(x,y,z))

is not, where  v denotes OR.

Every formula of first-order logic can be converted to an equivalent formula in prenex normal form.

This entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha


Chang, C.-L. and Lee, R. C.-T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.Kleene, S. C. Mathematical Logic. New York: Dover, 2002.

Referenced on Wolfram|Alpha

Prenex Normal Form

Cite this as:

Sakharov, Alex. "Prenex Normal Form." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein.

Subject classifications