Reference. Theorem. Rule induction [sterling-rule-induction-2025]

February 8, 2025
Sterling, Jon
https://jonmsterling.com/notes/0171

Backlinks

Definition. Rule induction [0027]

November 25, 2025

We let \(\mathcal R\) denote the set of syntactic rules over some set \(X\). Let \(X_\mathcal R \subseteq X\) be the closure of \(X\) under the rules in \(\mathcal R\). In other words: (1)

\[ (X_\mathcal R \in \text {Cl}_\mathcal R \land \forall S \in \text {Cl}_\mathcal R \to X_\mathcal R \subseteq S) \equiv (X_\mathcal R = \bigcap \text {Cl}_\mathcal R) \]

Proof of rule induction

November 25, 2025

Our proof here is defined in two parts:

Closed: We show that the set \(X_\mathcal R\) is closed under the rules in \(\mathcal R\). In other words, for every rule \((x_1, \ldots , x_n) \mapsto x \in \mathcal R\), if \(x_1, \ldots , x_n \in X_\mathcal R\), then \(x \in X_\mathcal R\).
Minimal: We show that \(X_\mathcal R\) is the smallest set closed under the rules in \(\mathcal R\). In other words, for any set \(S \subseteq X\) that is closed under the rules in \(\mathcal R\), we have \(X_\mathcal R \subseteq S\).

Proof.

November 25, 2025

We fix an arbitrary rule in \(\mathcal R\):

By definition of \(X_\mathcal R\), we have that \(x_1, \ldots , x_n \in X_\mathcal R\). Since \(X_\mathcal R\) is closed under the rules in \(\mathcal R\), it follows that \(x \in X_\mathcal R\). Thus, \(X_\mathcal R\) is closed under the rules in \(\mathcal R\).

Now we want to check that \(X_\mathcal R\) is the smallest set closed under the rules in \(\mathcal R\). Let \(S \subseteq X\) be an arbitrary set that is closed under the rules in \(\mathcal R\). We need to show that \(X_\mathcal R \subseteq S\). We can equivalently state this as:

Forall derivations \(d\) generated by rules in \(\mathcal R\), the conclusions of \(d\) are in \(S\).

Or in terms of the height of a derivation as:

Forall derivations \(d\) of height \(h\) generated by rules in \(\mathcal R\), the conclusions of \(d\) are in \(S\).

We proceed by induction on the height of the derivation \(d\).

In the base case any derivation has a height of at least 1, the base case holds vacuously.
In the inductive case we suppose that the conclusions of every derivation of height less than or equal to \(k\) are in \(S\). ; we must prove that the conclusion of any derivation of height \(k + 1\) is also in \(S\).

Let \(d\) be an arbitrary derivation of height \(k + 1\). By definition of derivation height, the last inference in \(d\) must be of the form:

where each sub-derivation \(d_i\) has height less than or equal to \(k\). By the inductive hypothesis, the conclusions of each sub-derivation \(d_i\) are in \(S\). Since \(S\) is closed under the rules in \(\mathcal R\), it follows that the conclusion \(x\) of the derivation \(d\) is also in \(S\).

Thus, by induction, we have shown that for all derivations \(d\) generated by rules in \(\mathcal R\), the conclusions of \(d\) are in \(S\). Therefore, \(X_\mathcal R \subseteq S\).

Tarski's fixpoint view

November 25, 2025

Another way we can view what this proof establishes is in terms of the monotone function \(f_\mathcal R: \mathcal P(X) \to \mathcal P(X)\) induced by the rules in \(\mathcal R\), defined as:

\[ f_\mathcal R(S) = \bigcup _{r \in \mathcal R} f_r(S) \]

The main fact this proof establishes is that the closure \(X_\mathcal R\) is the least fixed point of the function \(f_\mathcal R\), meaning that:

\[ f_\mathcal R(X_\mathcal R) = X_\mathcal R \land \forall S.\ f_\mathcal R(S) \subseteq S \implies X_\mathcal R \subseteq S \]

In other words \(X_\mathcal R\) is the smallest set of premises and conclusions that is closed under the rules in \(\mathcal R\). Naturally every other set closed under the rules must contain at least the members of \(X_\mathcal R\) (but possibly more).