---
title: Induction and Recursion on Formulas
module: Sentential Logic
moduleNumber: 2
lessonNumber: 4
order: 204
summary: >
  Two principles govern any set generated from initial elements by operations:
  prove a property of all its members by covering the initial elements and the
  closure steps, and define a function on it by recursion on structure. The
  recursion theorem needs the set to be freely generated, and unique readability
  supplies that condition for the well-formed formulas.
topics: [Sentential Logic]
sources:
  - book: Enderton
    ref: "Ch. 1 — Sentential Logic; §1.4 Induction and Recursion"
draft: false
---

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.[^enderton-recur]

## 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$.

> **Theorem.** $C^\ast = C_\ast$.

> **Proof.** For $C^\ast \subseteq C_\ast$, check $C_\ast$ is inductive: $B = C_1
> \subseteq C_\ast$, and if $x, y \in C_\ast$ then concatenating their construction
> sequences and appending $f(x, y)$ places $f(x, y)$ in $C_\ast$; similarly for $g$.
> For $C_\ast \subseteq C^\ast$, take a construction sequence $x_1, \dots, x_n$ and
> induct on $i$: $x_i$ is in $B \subseteq C^\ast$ or is built from earlier entries
> already in $C^\ast$, which is closed. $\blacksquare$

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

| $U$ | $B$ | operations | generated $C$ |
| --- | --- | --- | --- |
| reals | $\{0\}$ | successor $x \mapsto x+1$ | naturals $\{0,1,2,\dots\}$ |
| reals | $\{0\}$ | successor and predecessor | integers $\mathbb{Z}$ |
| real functions | identity, constants | $+,\ \cdot,\ \div$, roots | algebraic functions |
| expressions | sentence symbols | $\mathcal{E}_\neg, \mathcal{E}_\wedge, \mathcal{E}_\vee, \mathcal{E}_\to, \mathcal{E}_\leftrightarrow$ | wffs |

## The induction principle

Every generated set carries a proof method, generalizing the wff version from the
[formation
lesson](/logic/sentential-logic/formal-languages-and-well-formed-formulas).

> **Theorem (Induction principle for generated sets).** Let $C$ be generated from $B$ by $\mathcal{F}$. If
> $S \subseteq C$ contains $B$ and is closed under the operations in
> $\mathcal{F}$, then $S = C$.

> **Proof.** Such an $S$ is inductive, so $C = C^\ast \subseteq S$; the reverse
> inclusion is the hypothesis. $\blacksquare$

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.

> **Worked example.** In any wff, the number of places where a sentence symbol
> occurs exceeds the number of places where a binary connective occurs by exactly
> one: $s = c + 1$.
>
> Let $S$ be the set of wffs satisfying $s = c + 1$.
>
> - **Atoms.** A sentence symbol has $s = 1$ and $c = 0$, so $s = c + 1$.
> - **Negation.** $(\neg \alpha)$ adds neither a sentence symbol nor a binary
>   connective, so $s$ and $c$ match those of $\alpha$ and the equation is
>   inherited.
> - **Binary steps.** For $(\alpha \square \beta)$ one has $s = s_\alpha + s_\beta$
>   and $c = c_\alpha + c_\beta + 1$. Using $s_\alpha = c_\alpha + 1$ and
>   $s_\beta = c_\beta + 1$ gives
>   $s = (c_\alpha + 1) + (c_\beta + 1) = (c_\alpha + c_\beta + 1) + 1 = c + 1$.
>
> All five operations preserve membership in $S$, so by the induction principle
> $S$ is the set of all wffs.

$$
% caption: The shape of an induction on wffs: establish the property for the
% atoms, then show each formula-building operation preserves it; the induction
% principle closes the loop to all wffs.
\begin{tikzpicture}[font=\footnotesize,
  base/.style={draw=acc, minimum width=30mm, minimum height=10mm, align=center, font=\footnotesize},
  stp/.style={draw, minimum width=22mm, minimum height=9mm, align=center, font=\scriptsize}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[base] (b) at (0,0) {property holds\\of every atom};
  \node[stp] (s1) at (5,1.8)  {preserved by negation};
  \node[stp] (s2) at (5,0.6)  {preserved by conjunction};
  \node[stp] (s3) at (5,-0.6) {preserved by disjunction};
  \node[stp] (s4) at (5,-1.8) {preserved by the conditional};
  \node[stp] (s5) at (5,-3.0) {preserved by the biconditional};
  \node[base] (all) at (10,-0.6) {property holds\\of every formula};
  \foreach \s in {s1,s2,s3,s4,s5} \draw[->, black] (b.east) -- (\s.west);
  \foreach \s in {s1,s2,s3,s4,s5} \draw[->, black] (\s.east) -- (all.west);
\end{tikzpicture}
$$

## 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.

> **Example (Recursion can fail without free generation).** Let $U = \mathbb{R}$, $B = \{0\}$, $f(x,y) = x \cdot y$,
> $g(x) = x + 1$; then $C = \mathbb{N}$. Impose $h(0) = 0$, $h(f(x,y)) =
> f(h(x),h(y))$, and $h(g(x)) = h(x) + 2$. No such $h$ exists: $1 = g(0)$ forces
> $h(1) = 2$, while $1 = f(g(0), g(0))$ forces $h(1) = h(1)\cdot h(1) = 4$.

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.

$$
% caption: Why recursion can fail without free generation: an element reachable
% both as a product and as a successor gets two conflicting values, one from each
% rule, and no single function can satisfy both.
\begin{tikzpicture}[font=\footnotesize,
  n/.style={draw, circle, minimum size=9mm, inner sep=0pt, font=\footnotesize},
  r/.style={draw, minimum width=26mm, minimum height=9mm, align=center, font=\scriptsize}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[n, draw=acc, text=acc] (one) at (0,0) {1};
  \node[r] (asg) at (-4.4,1.3) {reached as a successor};
  \node[r] (asf) at (-4.4,-1.3) {reached as a product};
  \draw[->, black] (asg.east) -- (one.north west);
  \draw[->, black] (asf.east) -- (one.south west);
  \node[r, draw=acc] (v1) at (4.4,1.3) {rule wants value 2};
  \node[r, draw=acc] (v2) at (4.4,-1.3) {rule wants value 4};
  \draw[->, black] (one.north east) -- (v1.west);
  \draw[->, black] (one.south east) -- (v2.west);
  \node[text=acc, font=\footnotesize] at (4.4,0) {clash};
\end{tikzpicture}
$$

### Free generation

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

> **Definition (Freely generated).** $C$ is **freely generated** from $B$ by $f$
> and $g$ iff, restricted to $C$: (1) $f$ and $g$ are one-to-one, and (2) the
> range of $f$, the range of $g$, and the set $B$ are pairwise disjoint.

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

> **Theorem (Recursion).** Suppose $C$ is freely generated from $B$ by
> $f : U\times U \to U$ and $g : U \to U$. Let $V$ be any set and let
> $\bar h : B \to V$, $F : V \times V \to V$, $G : V \to V$ be functions. Then
> there is a **unique** $h : C \to V$ with
> $$
> h(x) = \bar h(x) \ \text{ for } x \in B, \qquad
> h(f(x,y)) = F(h(x), h(y)), \qquad h(g(x)) = G(h(x)).
> $$

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.

$$
% caption: The recursion theorem as unique extension: a map on the generators
% lifts to a homomorphism on the whole generated set, sending each built element
% f(x,y) to the value F applied to the values of its parts.
\begin{tikzpicture}[font=\footnotesize,
  s/.style={draw, minimum width=30mm, minimum height=12mm, align=center, font=\footnotesize}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[s] (C) at (0,0) {generated set\\(operations f, g)};
  \node[s] (V) at (6.4,0) {values\\(operations F, G)};
  \draw[->, draw=acc, thick] (C) -- node[above, font=\scriptsize, text=acc] {unique homomorphism} node[below, font=\scriptsize, text=acc] {extends the map on B} (V);
  \node[s] (B) at (0,-2.6) {generators B};
  \node[s] (VB) at (6.4,-2.6) {chosen values};
  \draw[->, black] (B) -- node[above, font=\scriptsize] {given map} (VB);
  \draw[->, black] (B) -- (C);
  \draw[->, black] (VB) -- (V);
\end{tikzpicture}
$$

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.[^enderton-recur]

## Wffs are freely generated

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

> **Theorem (Unique readability).** The five formula-building operations, restricted
> to wffs, are one-to-one and have pairwise-disjoint ranges disjoint from the
> sentence symbols. That is, the set of wffs is freely generated from the sentence
> symbols by the five operations.

> **Proof.** If $(\alpha \wedge \beta) = (\gamma \wedge \delta)$ with all four
> wffs, delete the leading $($ to get $\alpha \wedge \beta) = \gamma \wedge
> \delta)$; by the initial-segment lemma neither of $\alpha, \gamma$ can be a proper initial segment
> of the other, so $\alpha = \gamma$ and then $\beta = \delta$ — the operation is
> injective. If $(\alpha \wedge \beta) = (\gamma \to \delta)$, the same reasoning
> gives $\alpha = \gamma$, forcing $\wedge = \to$, impossible; so distinct
> operations have disjoint ranges. A negation begins $(\neg$, which no conjunction
> does, and no sentence symbol begins with $($. $\blacksquare$

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.

> **Worked example.** Compute the length of $((\neg A) \to B)$ from the length
> recursion $h(\text{symbol}) = 1$, $h((\neg\alpha)) = 3 + h(\alpha)$,
> $h((\alpha \to \beta)) = 3 + h(\alpha) + h(\beta)$.
>
> $$
> h((\neg A)) = 3 + h(A) = 4, \qquad
> h(((\neg A) \to B)) = 3 + h((\neg A)) + h(B) = 3 + 4 + 1 = 8.
> $$
>
> Counting the eight symbols of $((\neg A) \to B)$ directly agrees. Because the
> wff is freely generated, the two constructions it might have been given cannot
> disagree — there is only one — so the length is unambiguous.

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.

$$
% caption: The chain of dependence behind a well-defined truth valuation, each
% step licensing the next.
\begin{tikzpicture}[font=\footnotesize,
  s/.style={draw, minimum width=32mm, minimum height=11mm, align=center, font=\scriptsize}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[s] (ur) at (0,0) {unique\\readability};
  \node[s] (fg) at (3.7,0) {formulas freely\\generated};
  \node[s] (rt) at (7.4,0) {recursion\\theorem applies};
  \node[s, draw=acc, text=acc] (v) at (11.1,0) {valuation\\unambiguous};
  \draw[->, black] (ur) -- (fg);
  \draw[->, black] (fg) -- (rt);
  \draw[->, draw=acc] (rt) -- (v);
\end{tikzpicture}
$$

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

[^enderton-recur]: Enderton, §1.4 — generated sets (top-down and bottom-up), the induction principle, the recursion theorem with its freeness hypothesis and proof by acceptable approximating functions, the non-freely-generated failure, and the unique readability theorem identifying wffs as freely generated.