The normal form algorithm and its applications

The lesson on normal forms gave two proofs of their existence. The first goes through the truth table, which has $2^n$ rows for $n$ variables; the second runs through the formula from the variables, following its single formation rule. Neither of them says how to proceed with a formula written with implications, biconditionals and nested negations, which is how formulas usually present themselves. If this is so, what is missing is a procedure that works on the written form itself, that can be carried out without thinking, that is known to terminate and that yields an equivalent formula. That is an algorithm, and its study is the first object of this lesson; the second is what is done with it: describing with formulas the behavior of a device and building a circuit that reproduces it.

Written forms and replacement

Recall that the formulas of the course are strings of circles and disks, and that $\neg$, $\vee$, $\wedge$, $\rightarrow$, $\leftrightarrow$ and $\veebar$ are abbreviations defined from joint denial (lesson on the language of propositional logic). When we write $((p \vee q) \rightarrow (\neg q \wedge p))$ we do not write the string, but a written form of it: a tree whose leaves are variables and whose nodes are the connectives $\neg$, $\wedge$, $\vee$, $\rightarrow$, $\leftrightarrow$, $\veebar$ and $\downarrow$, each with its components. Every written form designates a single formula, the one that results from unfolding its abbreviations; and one and the same formula can have several written forms: the lesson on normal forms observed that $\neg\neg\varphi$ and $(\varphi \vee \varphi)$ are the same string. The algorithm reads the written form, not the string; that is why it pays to distinguish them. Since the distinction matters only for knowing where each step acts, we shall use the letters $\varphi$, $\psi$, $\chi$ for written forms and for the formulas they designate, and we shall write $\varphi \eqsem \psi$ when the designated formulas are semantically equivalent. A written subform of a written form is the subtree hanging from one of its nodes.

A step of the algorithm replaces one written subform by another. The instrument that guarantees that this change does not alter the meaning is the semantic replacement theorem of the lesson on semantic consequence and equivalence; but that theorem replaces one occurrence in the string, and a written subform may correspond to several occurrences in the string, because each abbreviation copies its components: in $(\varphi \vee \psi) = ((\varphi \downarrow \psi) \downarrow (\varphi \downarrow \psi))$, the component $\varphi$ appears twice. The following lemma adapts replacement to written forms.

Here $F_c$ is the truth function of the connective: $F_\neg(a) = 1 - a$, $F_\wedge(a, b) = ab$, and so on for the others. The same result is obtained from the semantic replacement theorem by applying it once for each copy of $\theta$ in the string and chaining the equivalences by transitivity; the proof through the written form is shorter because it counts the written connectives and not the copies.