In first-order logic, normal forms are still useful for providing a notion of a canonical form. However, their other benefit of corresponding closely to truth tables does not apply here, since truth tables aren't useful for first-order logic.
A formula in Prenex Conjunctive Normal Form, or PrenexCNF, has a body in CNF preceded by a series of quantifiers. Similarly, a formula in PrenexDisjunctiveNormalForm, or Prenex DNF, has a body in DNF preceded by a series of quantifiers.
Example 4.10
Assuming φ is in CNF, then the following are each in prenex CNF. On the other hand, if φ is in DNF, these are in prenex DNF.
- φ
- ∀x.φ
- ∃x.∀y.∃z.φ
Every formula has an equivalent prenex CNF formula and equivalent prenex CNF formula. For brevity, we'll skip proving this.
- 2216 reads
