Theorem·T06
The Peano axioms
Zero, successor, injectivity, and induction: arithmetic stands on ZFC ground.
In words
Zero is a natural number; the successor of every natural number is again a natural number; no successor equals zero; two naturals with the same successor are equal; and induction holds.
Never needed: F05 · F10 · F11 · F12 · F13 · A02 · A03 · A04 · A05 · A06 · A07 (computed from the citation graph, not asserted).
Proof
- 1
- 2(P3): , since contains (D006, D003). If then by substitutivity, contradicting D002 (negation). So .
- 3(P4): Assume . From : either or . Symmetrically, from : either or (substitutivity).
- 4If we are done. Otherwise both disjunctions fall to their first case: and , which is a two-element membership cycle, impossible by L05 (ii). So (disjunction elimination, excluded middle).
- 5
∎
Remarks
Dedekind (1888) and Peano (1889) proposed these as axioms characterizing the naturals; inside ZFC they become theorems about the explicitly constructed set ω. The five properties are all the arithmetic that is ever needed: the recursion theorem turns them into definitions of addition and multiplication, and everything from commutativity to the infinitude of primes follows. Dedekind also showed the axioms are categorical: any two structures satisfying them are isomorphic, so they pin down the naturals completely.