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

(1)

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

For example, the formula

(2)

is in prenex normal form, whereas formula

(3)

is not, where 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)

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.

CITE THIS AS:

Sakharov, Alex. "Prenex Normal Form." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein. http://mathworld.wolfram.com/PrenexNormalForm.html