Table of Contents

1. Propositional Logic
2. Valuations
3. Disjunctive Normal Form
4. Conjunctive Normal Form
5. Implication Equivalence
6. Biconditional Equivalence
7. De Morgan’s Laws
8. Why CNF and DNF Matter

This chapter stands alone as a mathematical reference. If you’re only interested in the code, chapters 1–4 cover the complete implementation. Here we formalize the ideas and prove that they work.

Propositional Logic

Propositional variables are symbols - $p, q, r, \ldots$ - that can be either true ($\top$) or false ($\bot$).

A well-formed formula (wff) is built inductively:

1. Every propositional variable is a wff.
2. If $\varphi$ is a wff, then $\lnot \varphi$ is a wff.
3. If $\varphi$ and $\psi$ are wffs, then $(\varphi \land \psi)$, $(\varphi \lor \psi)$, $(\varphi \to \psi)$, and $(\varphi \leftrightarrow \psi)$ are wffs.

We write $\operatorname{Var}(\varphi)$ for the set of propositional variables appearing in $\varphi$.

Valuations

A valuation (or assignment) is a function $v \colon \operatorname{Var}(\varphi) \to \{\top, \bot\}$. Given a valuation, the truth value of a formula is determined recursively:

A formula $\varphi$ is a tautology if $v(\varphi) = \top$ for every valuation $v$. Two formulas $\varphi$ and $\psi$ are logically equivalent, written $\varphi \equiv \psi$, if $v(\varphi) = v(\psi)$ for every valuation $v$.

Disjunctive Normal Form

A literal is a variable $p$ or its negation $\lnot p$. A minterm over variables $p_1, \ldots, p_n$ is a conjunction of $n$ literals, one per variable:

where each $\ell_i$ is either $p_i$ or $\lnot p_i$.

A formula is in Disjunctive Normal Form (DNF) if it is a disjunction of minterms:

Theorem. Every formula $\varphi$ has an equivalent DNF.

Proof. Let $\operatorname{Var}(\varphi) = \{p_1, \ldots, p_n\}$. Consider all $2^n$ valuations. For each valuation $v$ where $v(\varphi) = \top$, define a minterm:

where $\ell_i^v = p_i$ if $v(p_i) = \top$, and $\ell_i^v = \lnot p_i$ if $v(p_i) = \bot$.

Define $\varphi_{\text{DNF}} = \bigvee_{v : v(\varphi) = \top} m_v$. If no valuation satisfies $\varphi$, set $\varphi_{\text{DNF}} = \bot$ (which is equivalent since $\varphi$ is unsatisfiable).

We claim $\varphi_{\text{DNF}} \equiv \varphi$. Let $w$ be any valuation:

• If $w(\varphi) = \top$: then $m_w$ is one of the disjuncts, and $w(m_w) = \top$ since each literal in $m_w$ matches $w$. So $w(\varphi_{\text{DNF}}) = \top$.

• If $w(\varphi) = \bot$: then $m_w$ is not a disjunct. For any other minterm $m_v$ in $\varphi_{\text{DNF}}$, since $v \neq w$ on at least one variable, at least one literal in $m_v$ evaluates to $\bot$ under $w$, making $w(m_v) = \bot$. Since all disjuncts are $\bot$, $w(\varphi_{\text{DNF}}) = \bot$.

Therefore $\varphi_{\text{DNF}} \equiv \varphi$. $\blacksquare$

Connection to code:

This is exactly what our code does in Chapter 4: for each TRUE row in the truth table, we build a minterm from the variable values in that row, then OR all the minterms together.

Conjunctive Normal Form

A maxterm over variables $p_1, \ldots, p_n$ is a disjunction of $n$ literals:

A formula is in Conjunctive Normal Form (CNF) if it is a conjunction of maxterms:

Theorem. Every formula $\varphi$ has an equivalent CNF.

Proof. For each valuation $v$ where $v(\varphi) = \bot$, define a maxterm:

where $\ell_i^v = \lnot p_i$ if $v(p_i) = \top$, and $\ell_i^v = p_i$ if $v(p_i) = \bot$.

Note the flipped literal construction compared to DNF.

Define $\varphi_{\text{CNF}} = \bigwedge_{v : v(\varphi) = \bot} M_v$. If no valuation falsifies $\varphi$, set $\varphi_{\text{CNF}} = \top$.

We claim $\varphi_{\text{CNF}} \equiv \varphi$. Let $w$ be any valuation:

• If $w(\varphi) = \top$: for every maxterm $M_v$ in $\varphi_{\text{CNF}}$, we have $v \neq w$ on at least one variable $p_i$. If $v(p_i) = \top$ then $\ell_i^v = \lnot p_i$ and $w(p_i) = \bot$… wait, that doesn’t help directly. Instead: since $v(p_i) \neq w(p_i)$ for some $i$, the literal $\ell_i^v$ evaluates to $\top$ under $w$. To see why: if $v(p_i) = \top$, then $\ell_i^v = \lnot p_i$ and $w(p_i) = \bot$ (since they differ), so $w(\lnot p_i) = \top$. If $v(p_i) = \bot$, then $\ell_i^v = p_i$ and $w(p_i) = \top$, so $w(p_i) = \top$. Either way, at least one literal in $M_v$ is $\top$, so $w(M_v) = \top$. Since all maxterms are $\top$, $w(\varphi_{\text{CNF}}) = \top$.

• If $w(\varphi) = \bot$: then $M_w$ is one of the conjuncts. Every literal in $M_w$ evaluates to $\bot$ under $w$: if $w(p_i) = \top$, then $\ell_i^w = \lnot p_i$ and $w(\lnot p_i) = \bot$; if $w(p_i) = \bot$, then $\ell_i^w = p_i$ and $w(p_i) = \bot$. So $w(M_w) = \bot$, which makes $w(\varphi_{\text{CNF}}) = \bot$.

Therefore $\varphi_{\text{CNF}} \equiv \varphi$. $\blacksquare$

Connection to code:

This matches our code: for each FALSE row, we build a maxterm with flipped literals (negate the trues, keep the falses), then AND all maxterms together.

Implication Equivalence

Our evaluator implements implication as !left || right. Here’s the formal justification.

Theorem. $A \to B \equiv \lnot A \lor B$.

Proof. We verify by truth table:

The columns match on all rows, so $A \to B \equiv \lnot A \lor B$. $\blacksquare$

Biconditional Equivalence

Theorem. $A \leftrightarrow B \equiv (A \to B) \land (B \to A)$.

Proof. Again by truth table:

The columns match. $\blacksquare$

Using the implication equivalence, we can also write:

Our code uses === on booleans for equiv, which is equivalent to checking both implications simultaneously.

De Morgan’s Laws

Theorem (De Morgan). For any formulas $A$ and $B$:

Proof. Truth tables for the first law:

The columns $\lnot(A \land B)$ and $\lnot A \lor \lnot B$ match.

The second law follows by similar verification (or by applying the first law to $\lnot A$ and $\lnot B$ and simplifying). $\blacksquare$

De Morgan’s laws are fundamental in logic - they let us push negation through conjunctions and disjunctions. While our calculator doesn’t need them for the basic algorithm (we build normal forms directly from the truth table), they are essential if you ever want to simplify or manipulate CNF/DNF expressions.

Why CNF and DNF Matter

Normal forms aren’t just a theoretical curiosity. They have practical applications across computer science:

SAT solvers. Most modern SAT solvers (used in hardware verification, planning, cryptanalysis, and more) expect their input in CNF. The DPLL and CDCL algorithms that power these solvers operate directly on conjunctions of clauses.

Circuit design. In digital electronics, DNF corresponds directly to a sum-of-products implementation (OR gates combining AND gates), while CNF corresponds to a product-of-sums (AND gates combining OR gates). Converting to normal form is a standard step in circuit synthesis.

Logic simplification. Normal forms provide a starting point for minimization algorithms like Quine–McCluskey or Espresso, which reduce the number of terms while preserving logical equivalence.

Databases. Query optimization sometimes involves converting conditions to CNF for efficient index utilization.

The truth table method we implemented gives us a canonical normal form (one unique representation for each truth function), which is correct but can be exponentially large. In practice, specialized algorithms exist for more compact representations. But the truth table approach is the clearest way to understand what CNF and DNF are, which is why we started here.

Previous: Chapter 4: Truth Tables and Normal Forms

Series: Back to Truth Table, CNF, and DNF Generator