Theorem·T05
Mathematical induction
To prove something for every natural: check zero, and pass it along successors.
For every
:
where
is the set of natural numbers and
the successor.
In words
If A contains zero and, for every n, whenever n is in A the successor of n is in A as well, then A is the whole set of natural numbers.
Never needed: F03 · F04 · F05 · F06 · F08 · F10 · F11 · F12 · F13 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Proof
- 1Assume and . These are exactly the two clauses of D025, so is an inductive set.
- 2By L04 (ii), . By hypothesis . Mutual inclusion is equality by Extensionality (via D001): .
∎
Remarks
The workhorse of the whole library. To prove a property
for all naturals, form
by Separation and check the two hypotheses: the base case
and the induction step
; the theorem then gives
, that is,
holds everywhere. This is the fifth of the Peano axioms, here a theorem because ω was built as the least inductive set. A strengthening where the step may assume the property for all smaller numbers is strong induction.