We now have relations defined by inference rules — evaluation e \Downarrow v, typing \vdash e : \tau, and so on. The obvious next question is: how do we prove something true of every derivable judgement, when there are infinitely many of them? We cannot check them one by one. The answer is the single most important proof technique in the whole field: induction — and specifically rule induction (induction on derivations), the tool that turns "the relation is the least set closed under the rules" into a licence to prove universal statements.

You already know its baby brother. Ordinary mathematical induction proves P(n) for all naturals by checking P(0) and "P(n) \Rightarrow P(n+1)". Structural induction generalises this from numbers to inductively-defined data (our expression trees); rule induction generalises it once more, to derivations built from inference rules. All three are the same idea — cover a base case, then an inductive step for each way of building something bigger — differing only in what you are inducting over.

Structural induction on syntax

Recall our expressions are the least set with numerals n as base cases and e_1 + e_2, e_1 \times e_2 as inductive cases. Structural induction proves a property P(e) holds for all expressions by matching that shape:

Do all three and you have P(e) for every expression — because every expression is built by finitely many applications of exactly these constructors, and induction chases the proof down through its subtrees to the leaves. The pattern is one case per constructor, mirroring the datatype's variants: the same shape as the recursion that defines functions over the tree. Definition and proof march in lockstep.

Rule induction: induction on the derivation

Structural induction inducts on the expression. Sometimes we instead need to induct on the derivation of a judgement — the proof tree itself — because the property is about the derivation, or because the relation is not driven purely by one syntactic argument. This is rule induction, and it comes straight from the "least closed set" definition: to prove a property P holds of every derivable judgement, show that the set of judgements satisfying P is itself closed under the rules. Concretely:

Here is the inductive step for the (E-Add) rule, drawn out — the premises carry the induction hypothesis, and the conclusion is the goal:

Why is this valid? Because the relation is the least set closed under the rules. The judgements satisfying P form a set; the bullets above say exactly that this set is closed under every rule; and the least closed set is contained in any closed set. So every derivable judgement satisfies P. The induction hypothesis is legitimate for the same reason it is in ordinary induction: each premise J_i has a strictly smaller sub-derivation than the conclusion, so we are always appealing to P on something we have "already reached".

A full worked proof: evaluation is deterministic

Let us prove a real theorem end to end — the kind of result a semantics exists to make provable. For our arithmetic language with rules (E-Num), (E-Add), (E-Mul):

Proof. By rule induction on the derivation of e \Downarrow v (equivalently, structural induction on e). Take the property

We consider each rule that could have concluded e \Downarrow v. Because the form of e determines which rule applies, this is a clean case split.

Case (E-Num). Here e = n and v = n. Suppose also n \Downarrow v'. The only rule whose conclusion can match a numeral n is (E-Num), which forces v' = n. Hence v = n = v'. (Base case — no induction hypothesis needed.)

Case (E-Add). Here e = e_1 + e_2, and the derivation ends in

The induction hypotheses are: P(e_1 \Downarrow v_1) and P(e_2 \Downarrow v_2) — i.e. e_1 and e_2 each evaluate to at most one value. Now suppose e_1 + e_2 \Downarrow v'. Since e is a syntactic sum, the only rule that can conclude this is (E-Add) again, so its derivation must have the form e_1 \Downarrow v_1', e_2 \Downarrow v_2' with v' = v_1' + v_2'. By the induction hypothesis on e_1, v_1 = v_1'; by the induction hypothesis on e_2, v_2 = v_2'. Therefore v = v_1 + v_2 = v_1' + v_2' = v'.

Case (E-Mul). Identical to (E-Add), with \times for +: the only rule concluding e_1 \times e_2 \Downarrow v' is (E-Mul), the induction hypotheses give v_1 = v_1' and v_2 = v_2', and so v = v_1 \times v_2 = v_1' \times v_2' = v'.

All rules are covered, so P holds for every derivation, which is exactly the theorem. \blacksquare

Notice the two ingredients that did all the work, and that recur in every such proof: an inversion step ("the only rule that could conclude this judgement is…", which relies on the relation being the least closed set) and the induction hypothesis applied to the strictly smaller sub-derivations. Learn this shape and you can prove type soundness, confluence, and the rest.

The proof, checked by exhaustion in code

We cannot run an infinite proof, but we can illustrate its claim: build the evaluator faithfully from the rules, then check on many random expressions that a second, independent evaluation always agrees — the concrete shadow of "at most one value". Press Run:

The count is always 0, of course — but that is the whole point of the theorem: the relation \Downarrow, which we defined with rules and could in principle have made ambiguous, is in fact a function. The proof told us so for all expressions at once; the code merely lets us watch it not fail.