Normal Form Existence (Propositional Logic)

Definition

Normal Form Existence (Propositional Logic)

Every propositional formula $F$ has an equivalent formula in conjunctive normal form and an equivalent formula in disjunctive normal form:

$$\forall F:\exists F_{\wedge }:F\equiv F_{\wedge }\in \mathrm{CNF},\exists F_{\vee }:F\equiv F_{\vee }\in \mathrm{DNF}.$$

The literature usually states this as an unremarkable proposition rather than a named theorem; “normal form theorem” and “CNF–DNF existence theorem” are the common labels.

Construction

Equivalence rewriting

Rewrite $F$ using the algebraic equivalences: eliminate $\to$ and $\leftrightarrow$, push negation inwards with De Morgan’s rules and double negation elimination, then distribute $\vee$ over $\wedge$ (for CNF) or $\wedge$ over $\vee$ (for DNF) using distributivity.

By truth table

Let $v$ range over the assignments of the atoms of $F$. For CNF, take the conjunction over all $v$ with $v(F)=v(\perp )$ of the clause $\bigvee \{L:v(L)=v(\perp )\}$ of false literals. For DNF, take the disjunction over all $v$ with $v(F)=v(\top )$ of the conjunction $\bigwedge \{L:v(L)=v(\top )\}$ of true literals.

Complexity

Warning

An equivalent CNF or DNF can be exponentially larger than $F$. If only satisfiability preservation is required, a CNF can be computed in linear time by introducing fresh atoms (definitional transformation).