Induction is recursion, read backwards
Every recursive function you have written is a proof by induction you did not know you were writing. Seeing the correspondence makes both halves easier.
A recursive function has a base case and a recursive case, and it terminates because each call moves strictly closer to the base. A proof by induction has a base case and an inductive step, and it is valid because every instance is reachable from the base in finitely many steps. These are not analogous. They are the same structure, written by two communities who mostly do not read each other.
The correspondence#
| Recursion | Induction |
|---|---|
| base case | base case |
| recursive case | inductive step |
| the recursive call's return value | the inductive hypothesis |
| termination measure | well-ordering of the index |
| the function's postcondition | the statement being proved |
The practical consequence is that anyone who can write a correct recursive function can write a proof by induction, and the step they find hard — 'am I allowed to just assume it holds for n?' — is a step they already take every time they trust a recursive call.
You do not verify the recursive call. You assume it works and check that the surrounding case is right. That assumption is the inductive hypothesis.
Strong induction, and why it is not stronger#
Strong induction assumes the statement for all values below n rather than just for n − 1. This looks like a more powerful principle and is not: each form can be derived from the other. What it is, is a more convenient one — and it corresponds exactly to a recursive function that may call itself on any smaller input rather than only on its immediate predecessor.
Merge sort is the canonical example on both sides. It recurses on halves, not on n − 1, so its correctness proof needs the hypothesis for all smaller sizes. Nobody finds the code surprising; the proof surprises people only because it is presented as a separate principle rather than as the same code with the types erased.
Where the correspondence breaks#
It breaks at infinity. A recursive function must terminate, so its measure must be well-founded and finite. Transfinite induction has no computational counterpart — there is no function you can run that recurses through the ordinals. For everything a program can actually do, though, the two are interchangeable, and treating them as one idea is worth more than treating them as two.