Theorem: Every propositional formula is logically equivalent to a formula in conjunctive normal form (CNF).

We prove this constructively by providing an algorithm to convert any formula to CNF.

Step 1: Eliminate implication and biconditional

Replace every occurrence of $\phi \to \psi$ with $\neg \phi \lor \psi$, and every occurrence of $\phi \leftrightarrow \psi$ with $(\neg \phi \lor \psi) \land (\phi \lor \neg \psi)$. These replacements are justified by logical equivalence. After this step, the formula contains only $\neg$, $\land$, and $\lor$.

Step 2: Push negations inward (De Morgan's Laws)

Repeatedly apply the following equivalences until all negations apply directly to propositional variables:

• $\neg \neg \phi \equiv \phi$ (double negation)
• $\neg(\phi \land \psi) \equiv \neg \phi \lor \neg \psi$ (De Morgan)
• $\neg(\phi \lor \psi) \equiv \neg \phi \land \neg \psi$ (De Morgan)

After this step, the formula is in negation normal form (NNF): only variables are negated, and the formula uses only $\land$ and $\lor$ (besides negations of variables).

Step 3: Distribute disjunction over conjunction

Repeatedly apply the distributive law:

and its symmetric version:

This moves all conjunctions to the outermost level and all disjunctions inside.

Step 4: Simplification (optional)

Remove redundant clauses and literals using:

• $\phi \land \phi \equiv \phi$ (idempotency)
• $\phi \lor \phi \equiv \phi$ (idempotency)
• $\phi \lor \neg \phi \equiv \top$ (excluded middle)
• If a clause contains both $p$ and $\neg p$, it can be removed (tautological clause)

Example: Convert $\phi = \neg((p \to q) \land \neg r)$ to CNF.

1. Eliminate implication: $\neg((\neg p \lor q) \land \neg r)$
2. Apply De Morgan: $\neg(\neg p \lor q) \lor \neg \neg r$
3. Apply De Morgan and double negation: $(p \land \neg q) \lor r$
4. Distribute: $(p \lor r) \land (\neg q \lor r)$

The result is in CNF.

Correctness: Each transformation preserves logical equivalence, so the final CNF formula is equivalent to the original. The algorithm terminates because each step either reduces the formula size (eliminating connectives) or moves the structure closer to CNF without increasing formula depth beyond a bounded limit.

Complexity: The CNF conversion can exponentially increase formula size in the worst case. For example, a formula with structure $(a_1 \lor b_1) \land (a_2 \lor b_2) \land \cdots \land (a_n \lor b_n)$ is already in CNF, but its "dual" formed by swapping $\land$ and $\lor$ requires $2^n$ clauses when converted to CNF.