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