Theorem·T09
The well-ordering principle
Every non-empty set of naturals has a smallest member.
For every
:
and this least element
is
. Order from D029.
In words
For any set S of natural numbers: if S is not empty then there is some m that belongs to S and is at most every member of S. This least element is unique.
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1We prove the contrapositive: if has no least element, then .
- 2Let (Separation). We verify the hypothesis of strong induction for : let and suppose every lies in , i.e. no belongs to .
- 3
- 4T08 gives . Since and every natural is outside , no member of exists: by Extensionality with D002. Contraposing (F04, excluded middle): a non-empty has a least element.
- 5Uniqueness: if and are both least, then (as ) and (as ). If , both inequalities are strict, giving and , which L16 forbids. So .
∎
Remarks
The well-ordering principle is the third face of induction: ordinary induction, strong induction and well-ordering are all equivalent over the naturals. It grounds every "take the least counterexample" argument, also known as infinite descent: if counterexamples existed, a least one would, and deriving a smaller one is then a contradiction. The division algorithm and prime divisor existence can both be run this way. The property is special: the integers, rationals and reals all fail it, which is why induction is a phenomenon of
.