Goodstein's theorem

Goodstein's theorem states that every Goodstein sequence eventually reaches zero, despite its terms initially growing rapidly. Its termination is independent of Peano arithmetic: the theorem is true but unprovable there.

Goodstein sequence: A sequence of natural numbers formed by hereditary base notation, base increases, and subtraction of one. The theorem asserts that every sequence generated by these rules terminates.
Peano arithmetic: A formal theory of the natural numbers based on axioms for zero, successor, and arithmetic operations. Goodstein's theorem is true but has no proof in this theory.
Reuben Goodstein: A British mathematician known for work in mathematical logic and the sequence theorem bearing his name. He introduced the sequences and proved their eventual termination.
Epsilon naught: The smallest ordinal alpha satisfying omega raised to alpha equals alpha. The ordinal descent associated with Goodstein sequences reaches below this proof-theoretic boundary.
Hereditary base notation: A numeral representation in which exponents are recursively expressed in the same base. Goodstein's rule changes the base throughout each term's nested representation.
Primitive recursion: A method for defining functions by initial values and repeated application of a recursion rule. The sequence operations are elementary to specify even when their growth is immense.
Kirby–Paris theorem: A result that the hydra game terminates, while its termination is unprovable in Peano arithmetic. Its proof-theoretic behavior parallels Goodstein's theorem and helped establish the phenomenon's reach.
Proof-theoretic ordinal: An ordinal measuring the transfinite induction a formal theory can justify. Goodstein's theorem illustrates how ordinal strength calibrates arithmetic unprovability.
Ordinal number: An ordinal is an order type extending the natural numbers to describe well-ordered sets. Replacing each sequence term's base with omega yields a strictly descending ordinal measure.
Mathematical induction: A proof method establishing a property for all natural numbers from a base case and a successor step. Peano arithmetic formalizes induction over natural numbers, but not every ordinal descent needed here.

Linked from 6 pages