Induction and Recursion on Formulas

Three constructions so far share a shape. The set of wffs is generated from sentence symbols by the formula-building operations; a property is proved of all wffs by checking the atoms and the operations; and the truth valuation $\bar{v}$ is defined by recursion on a formula's structure. Treated abstractly, the pattern yields an induction principle and a recursion theorem that apply to any generated set at once. The abstraction isolates the precise condition — free generation — under which definition by recursion is legitimate, and shows that wffs meet that condition precisely because they are uniquely readable.¹

Generated sets

Fix a set $U$, a subset $B\subseteq U$ of initial elements, and a class $\mathcal{F}$ of operations on $U$. To keep notation light, take $\mathcal{F}=\{f,g\}$ with a binary $f:U\times U\to U$ and a unary $g:U\to U$; the general case is the same. The set generated from $B$ by $\mathcal{F}$, written $C$, is meant to contain everything reachable from $B$ by applying $f$ and $g$ finitely often. Two definitions make this precise, one descending and one ascending.

• Top-down. Call $S\subseteq U$ inductive iff $B\subseteq S$ and $S$ is closed under $f$ and $g$. Let $C^{\ast }$ be the intersection of all inductive subsets of $U$. Then $C^{\ast }$ is itself inductive, and is the smallest inductive set: $x\in C^{\ast }$ iff $x$ belongs to every inductive set.
• Bottom-up. A construction sequence is a finite sequence $x_1,\dots ,x_n$ in which each $x_i$ is in $B$, or equals $f(x_j,x_k)$ for some $j,k<i$, or equals $g(x_j)$ for some $j<i$. Let $C_{\ast }$ be the set of endpoints of construction sequences. Writing $C_n$ for the endpoints of sequences of length $n$, we have $C_1=B$ and $C_1\subseteq C_2\subseteq \cdots$ with $C_{\ast }={\bigcup }_n{C}_n$.

The common value is written $C$, the set generated from $B$ by the operations.

The induction principle

Every generated set carries a proof method, generalizing the wff version from the formation lesson.

For wffs, $B$ is the set of sentence symbols and there are five operations, so a proof by induction has one base case and five inductive steps.

Definition by recursion

The harder direction is defining a function on $C$. Suppose we want $h$ on $C$ specified by rules: a value for $h(x)$ when $x\in B$, a rule computing $h(f(x,y))$ from $h(x)$ and $h(y)$, and a rule computing $h(g(x))$ from $h(x)$. The truth valuation follows this pattern, with $B$ the atoms and the rules the connective clauses.

At most one function can satisfy such rules — that is a quick induction. But existence can fail. The rules may contradict each other when an element of $C$ is reachable by two different constructions demanding two different values.

The trouble is that $1$ is built in two incompatible ways, and the two rules disagree there. Recursion needs each element of $C$ to have essentially one construction.

Free generation

The condition that rules out conflict is that the operations never collide.

Freeness says every element of $C$ arises in exactly one way — as an initial element, or as $f$ of a unique pair, or as $g$ of a unique element, never two of these at once. The naturals are freely generated from $\{0\}$ by the successor alone ($x\mapsto x+1$ is injective and $0$ is not a successor), but the integers are not freely generated by successor and predecessor: $2=S(S(0))$ and also $2=S(P(S(S(0))))$, so the earlier example's failure is generic.

The recursion theorem

Read algebraically, the conclusion says any map of the generators $B$ into $V$ extends uniquely to a homomorphism from $C$ (with operations $f,g$) into $V$ (with operations $F,G$). The value at each element is computed by climbing its construction and applying $F$ or $G$ at each step; freeness guarantees the answer does not depend on which construction is chosen, because there is only one.

The proof builds $h$ as the union of all acceptable partial functions — those defined on part of $C$ and consistent with the rules where defined. Set-theoretically one checks four claims: the union is single-valued (an induction), it is itself acceptable, its domain is all of $C$ (here freeness is used, to extend it past any $f(s,t)$ or $g(s)$), and it is unique (the set where two solutions agree is inductive). Freeness enters exactly at the domain step: it is what lets a partial solution be extended without contradiction.¹

Wffs are freely generated

The abstract theorem applies to sentential logic through one fact, which is unique readability restated.

With free generation in hand, the recursion theorem delivers the results the earlier lessons assumed.

• The truth valuation exists. Applying the recursion theorem with $V=\{F,T\}$, $\bar{h}=v$, and the connective clauses as $F$ and $G$ yields a unique $\bar{v}$ on all wffs — the missing existence half of the unique-extension theorem.
• Length is well defined. With $V=\mathbb{N}$, $\bar{h}(A)=1$, $h((\neg \alpha ))=3+h(\alpha )$, and $h((\alpha \wedge \beta ))=3+h(\alpha )+h(\beta )$ (similarly for the other binaries), $h$ computes the number of symbols in a wff.

The dependency is a short chain: unique readability makes the wffs freely generated; free generation makes the recursion theorem apply; the recursion theorem makes $\bar{v}$ well defined.

Induction on formulas and recursion on formulas now stand on a rigorous footing, free to be used without further comment.