TOPICS
Search

Prenex Normal Form


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

 Q_1x_1...Q_nx_nM,
(1)

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))
(2)

is in prenex normal form, whereas formula

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

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

References

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. https://mathworld.wolfram.com/PrenexNormalForm.html

Subject classifications