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) \]

1. Proof of rule induction

  • November 25, 2025

Our proof here is defined in two parts:

  1. 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\).
  2. 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\).

2. 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).

References

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

    Related

      Definition. Closure of a syntactic rule [002i]

      • November 26, 2025

      A syntactic rule on a set \(X\) expresses a closure condition (or operator) on the subsets of \(X\), which is to say on the elements of the power set \(\mathcal {P}\). In particular, we can say that for a particular subset \(S \in \mathcal {P}(X)\), we have that:

      \[ \{S \subseteq X \mid x_1,\ldots ,x_n \in S \to x \in S\} \]

      When we have a set \(\mathcal R\) denoting a set of rules over \(X\), we will write:

      \[ \text {Cl}_\mathcal R \in \mathcal P(X) \]

      to denote the intersection of the closure conditions expressed by each rule in \(\mathcal R\). In other words, the set of subsets of \(X\) that are closed under all the rules in \(\mathcal R\). Intuitively this set denotes all set's which satisfy the premises of the rule and hence can derive the conclusion. A particular rule \(r \in \mathcal R\) is said to determine a monotone function \(f_r: \mathcal P(X) \to \mathcal P(X)\) such that for any subset \(S \subseteq X\), we have that:

      \[ f_r(S) = \{x \in X \mid x_1, \ldots , x_n \in S\} \]

      What this function expresses is that if we know the assertions \(x_1\) to \(x_n\) are true (are in \(S\)) then we can additionally conclude \(x\) is true. A more pedantic equivalent version of this function is:

      \[ f_r(S) = S \cup \{x \in X \mid x_1, \ldots , x_n \in S\} \]

      There seems to be a general tendency to prefer the first version as it emphasizes the idea of the derivation of new conclusions from premises, however the second version is what's pedantically accurate in that we are accumulating the conclusion \(x\) into the set \(S\) based on the existing premises.

      Furthermore we have that the set \(\mathcal R\) of rules induces a monotone function that collectively closes up under each rule in the set as follows:

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

      What this function expresses is that for any subset \(S \subseteq X\), we can apply each rule in \(\mathcal R\) to \(S\) and take the union of all the resulting sets. This gives us the smallest superset of \(S\) closed under \(\mathcal R\). Intuitively it expresses all derivable conclusions \(x\) from premises \(x_1, \ldots , x_n\) in \(S\) according to the rules in \(\mathcal R\). In other words it corresponds to the idea of enumerating all rules for our given set \(S\) and seeing if we can add any new conclusions to \(S\) based on the premises already in \(S\).

      The closure of the set \(X\) under the rules in \(\mathcal R\), denoted by \(X_\mathcal R\), is then defined as the least fixpoint (or least pre-fixed point) of the function \(f_\mathcal R\):

      \[ \mu f_\mathcal R = \bigcap \ \{ S \subseteq X \mid f_\mathcal R(S) \subseteq S \} \]

      Definition. Closure operator [002f]

      • November 26, 2025

      A closure operator on a set \(S\) is a function \(\text {Cl} : \mathcal P(S) \to \mathcal P(S)\) from the powerset of \(S\) to itself that satisfies the following three properties for all subsets \(A, B \subseteq S\):

      • The operator is extensive meaning that the closure of a set always contains the set itself: \[ A \subseteq \text {Cl}(A) \]
      • The operator is idempotent meaning that applying the closure operator twice is the same as applying it once: \[ \text {Cl}(\text {Cl}(A)) = \text {Cl}(A) \]
      • The operator is monotone meaning that if one set is a subset of another, then the closure of the first set is a subset of the closure of the second set: \[ A \subseteq B \implies \text {Cl}(A) \subseteq \text {Cl}(B) \]

      We say that the closure of a subset is the result of the closure operator beingapplied to that subset. The closure of this subset under some operation is the smallest superset of the subset which is closed (i.e., remains within the superset when the operation is applied). It's also sometimes called the span (such as in linear algebra), generated set, or hull.

      Definition. Monotone function [0029]

      • November 25, 2025

      A monotone function (or monotone map) between two preorders \((A, \leq _A)\) and \((B, \leq _B)\) is a function \(f: A \to B\) that preserves the order relation. This means that for all elements \(x, y \in A\), if \(x \leq _A y\), then it must also hold that \(f(x) \leq _B f(y)\). In other words, the function \(f\) does not reverse the order of elements when mapping them from set \(A\) to set \(B\). Formally:(1)

      \[ \forall x, y \in A.\ x \leq _A y \implies f(x) \leq _B f(y) \]

      Definition. Tarski's Theorem [002b]

      • November 25, 2025

      We define a set \(X\), let \(\mathcal L(X)\) be the complete lattice of all subsets of \(X\) ordered by inclusion. A function \(f: \mathcal L(X) \to \mathcal L(X)\) is said to be monotone in this instance if it preserves inclusion which is to say that the following holds: (1)

      \[ A \subseteq B \subseteq X \implies f(A) \subseteq f(B) \]

      Pre-and-post fixed point

      • November 25, 2025

      For a monotone function \(f\) a pre-fixed point of \(f\) is a subset \(A \subseteq X\) such that \(f(A) \subseteq A\). Similarly, a post-fixed point of \(f\) is a subset \(B \subseteq X\) such that \(B \subseteq f(B)\).

      Conceptually the idea here is that the prefixed points are those sets in \(X\) where the function \(f\) maps to at most all members in \(A\). Conversely, the post-fixed points represent the subset where at least all members of the set are mapped to by other members of the same set. Another way to describe it would be that the pre-fixed points represent a closed or under-approximation of the function \(f\) while the post-fixed points represent a consistent or over-approximation of the function.

      A pre-fixed point of \(f\) is also said to be \(f\)-closed and a post-fixed point of \(f\) is said to be \(f\)-consistent.

      A least pre-fixed point of a monotone \(f\) is the smallest subset \(A \subseteq X\) such that \(f(A) \subseteq A\), denoted by \(\mu f\). Similarly, a greatest post-fixed point of \(f\) is the largest subset \(B \subseteq X\) such that \(B \subseteq f(B)\), denoted by \(\nu f\).

      Every monotone function \(f\) has a unique least pre-fixed point and a unique greatest post-fixed point given by the following equations:

      \[ \begin {align*} \mu f & = \bigcap \{ A \subseteq X \mid f(A) \subseteq A \} \\ \nu f & = \bigcup \{ B \subseteq X \mid B \subseteq f(B) \} \end {align*} \]

      Of note here is that the least pre-fixed point here corresponds to the closure of the function \(f\). That is to say that it is the smallest set which is closed under the function \(f\). Conversely, the greatest post-fixed point corresponds to the consistency of the function \(f\), being the largest set which is consistent with respect to \(f\).

      Lambek's lemma

      • November 25, 2025

      One thing we can observe is that \(\mu f\) is contained in all pre-fixed points of \(f\), by virtue of being the intersection, i.e. closure for all pre-fixed points. Furthermore, we have that \(\mu f\) is itself a pre-fixed point of \(f\)

      \[ f(\mu f) \subseteq \mu f \]

      and it is thereby the least pre-fixed point. To see this we note that if:

      \[ f(A ) \subseteq A \to f(\mu f) \subseteq A \]

      Explanation

      • November 25, 2025

      So the idea here is again that since \(A\) is a pre-fixed point of \(f\), by definition we have that \(f(A) \subseteq A\). The implication here is that if we apply \(f\) to our closure, the resulting set must still be within \(A\) since again we definitionally cannot have that \(f\) maps outside \(A\) so even if we constrain ourselves to some smaller set \(\mu f\) it doesn't negate the fact that \(f\) still cannot map outside \(A\).

      But by definition of \(\mu f\) we have that

      \[ \mu f \subseteq A \]

      Explanation

      • November 25, 2025

      This is more or less just restating the definition of \(\mu f\) as the intersection of all pre-fixed points of \(f\), which includes \(A\).

      Thus by monotonicity of \(f\) we have the following as required

      \[ f(\mu f) \subseteq f(A) \subseteq A \]

      Additionally we have

      \[ f(f(\mu f)) \subseteq f(\mu f) \]

      Which is to reiterate that \(f(\mu f)\) is itself a pre-fixed point of \(f\). Therefore, we have that

      \[ \mu f \subseteq f(\mu f) \]

      Explanation

      • November 25, 2025

      What this says at a high level; or what it implies given the above condition; is that the application of the monotone operator to the closure set \(\mu f\) doesn't shrink the set any further, in other words its operation stabilizes at this set such that each member in this set maps precisely to some other member in the set not more (i.e. outside as that would mean it's not closed) and not less (as that would imply it's not minimal).

      \[ f(\mu f) \subseteq \mu f \]

      What this says at a high level; or what it implies given the above condition; is that the application of the monotone operator to the closure set \(\mu f\) doesn't shrink the set any further, in other words its operation stabilizes at this set such that each member in this set maps precisely to some other member in the set not more (i.e. outside as that would mean it's not closed) and not less (as that would imply it's not minimal). A question I had here was:

      But why does this actually happen?

      A nice perspective to have firstly is seeing the set \(\mu f\) here as a generating set for the function \(f\). In other words if we view the function \(f\) as a set of rules which generate new members in the set from existing members, then the closure \(\mu f\) represents the most precise set of members which can be generated by these rules without introducing any extraneous members.

      The effect of this is that because the members in \(\mu f\) are precisely those which can be generated by the rules in \(f\), applying \(f\) to this set will simply regenerate the same members, hence why we have that \(\mu f \subseteq f(\mu f)\) since all the members in \(\mu f\) already correspond to members generated by the members of \(\mu f\) under the rules of \(f\)

      Furthermore, since we are working in the context of a complete lattice, as we take the intersection of more and more closed subsets under \(f\) we eventually reach a point where if we take some further intersection (move down more) we end up losing the closed property, but if we move up (i.e. take the union of more closed sets) we end up introducing extraneous members which violate the minimalism property, hence the idea that we stabilize at this set i.e. we are a fixed point on the lattice under the operator.

      The implication of this being that the closure \(\mu f\) is a fixed point of \(f\), and, because any fixed point is a pre-fixed point, it is the least pre-fixed point of \(f\). A dual argument shows that the greatest post-fixed point \(\nu f\) is also a fixed point of \(f\). This result is known as Lambek's lemma in Category theory.