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
WolframAlpha
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 FormCite this as:
Sakharov, Alex. "Prenex Normal Form." From MathWorld--A Wolfram Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/PrenexNormalForm.html