Theorem·T08
Strong induction
Assume the property below n, conclude it at n: then it holds everywhere.
For every
:
with
from D029.
In words
Suppose that for every n among the natural numbers, whenever S contains every m strictly below n it contains n itself. Then S is the whole set of natural numbers. No separate base case is needed: at zero the assumption is vacuously satisfied.
Never needed: F05 · F08 · F10 · F12 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1Assume the displayed hypothesis. Let by Separation: the set of up to which is already known to hold. We show by ordinary induction.
- 2
- 3Step: let , so every lies in . Any satisfies by L15 (iii), hence : the premise of the hypothesis holds at , so . Now every is either , hence , hence in ; or equal to . So .
- 4T05 yields . Finally, each satisfies , so by definition of : thus , and with , Extensionality gives (D001).
∎
Remarks
Also called complete induction or course-of-values induction. It looks stronger than ordinary induction (the step may use the property for all smaller numbers, not just the predecessor) but is proved from it by the classic trick of strengthening the statement to "everything up to
". Its natural habitat is arguments where the predecessor is useless but some smaller number is exactly what is needed, e.g. peeling a divisor off in L20. Equivalent, via contraposition, to the well-ordering principle.