Laurence Kirby and Jeff Paris[1] showed that it is unprovable in Peano arithmetic (but it can be proven in stronger systems, such as second-order arithmetic or Zermelo-Fraenkel set theory).
This was the third example of a true statement about natural numbers that is unprovable in Peano arithmetic, after the examples provided by Gödel's incompleteness theorem and Gerhard Gentzen's 1943 direct proof of the unprovability of ε0-induction in Peano arithmetic.
Kirby and Paris introduced a graph-theoretic hydra game with behavior similar to that of Goodstein sequences: the "Hydra" (named for the mythological multi-headed Hydra of Lerna) is a rooted tree, and a move consists of cutting off one of its "heads" (a branch of the tree), to which the hydra responds by growing a finite number of new heads according to certain rules.
Kirby and Paris proved that the Hydra will eventually be killed, regardless of the strategy that Hercules uses to chop off its heads, though this may take a very long time.
Just like for Goodstein sequences, Kirby and Paris showed that it cannot be proven in Peano arithmetic alone.
[1] Goodstein sequences are defined in terms of a concept called "hereditary base-n notation".
To achieve the ordinary base-n notation, where n is a natural number greater than 1, an arbitrary natural number m is written as a sum of multiples of powers of n: where each coefficient ai satisfies 0 ≤ ai < n, and ak ≠ 0.
For example, to achieve the base 2 notation, one writes Thus the base-2 representation of 35 is 100011, which means 25 + 2 + 1.
Similarly, 100 represented in base-3 is 10201: Note that the exponents themselves are not written in base-n notation.
Then rewrite any exponent inside the exponents in base-n notation (with the same limitation on the coefficients), and continue in this way until every number appearing in the expression (except the bases themselves) is written in base-n notation.
Similarly, 100 in hereditary base-3 notation is The Goodstein sequence
, write m in hereditary base-2 notation, change all the 2s to 3s, and then subtract 1 from the result.
doesn't give a good idea of just how quickly the elements of a Goodstein sequence can increase.
In spite of this rapid growth, Goodstein's theorem states that every Goodstein sequence eventually terminates at 0, no matter what the starting value is.
Goodstein's theorem can be proved (using techniques outside Peano arithmetic, see below) as follows: Given a Goodstein sequence G(m), we construct a parallel sequence P(m) of ordinal numbers in Cantor normal form which is strictly decreasing and terminates.
By infinite regress, G(m) must reach 0, which guarantees termination.
which computes the hereditary base k representation of u and then replaces each occurrence of the base k with the first infinite ordinal number ω.
Addition, multiplication and exponentiation of ordinal numbers are well defined.
Note that in order to calculate f(G(m)(n),n+1), we first need to write G(m)(n) in hereditary base n+1 notation, as for instance the expression
As the standard order < on ordinals is well-founded, an infinite strictly decreasing sequence cannot exist, or equivalently, every strictly decreasing sequence of ordinals terminates (and cannot be infinite).
It makes use of countable nonstandard models of Peano arithmetic.
The above proof still works if the definition of the Goodstein sequence is changed so that the base-changing operation replaces each occurrence of the base b with b + 2 instead of b + 1.
The extended version is in fact the one considered in Goodstein's original paper,[3] where Goodstein proved that it is equivalent to the restricted ordinal theorem (i.e. the claim that transfinite induction below ε0 is valid), and gave a finitist proof for the case where
The extended Goodstein's theorem without any restriction on the sequence bn is not formalizable in Peano arithmetic (PA), since such an arbitrary infinite sequence cannot be represented in PA.
This seems to be what kept Goodstein from claiming back in 1944 that the extended Goodstein's theorem is unprovable in PA due to Gödel's second incompleteness theorem and Gentzen's proof of the consistency of PA using ε0-induction.
[4] However, inspection of Gentzen's proof shows that it only needs the fact that there is no primitive recursive strictly decreasing infinite sequence of ordinals, so limiting bn to primitive recursive sequences would have allowed Goodstein to prove an unprovability result.
[4] Furthermore, with the relatively elementary technique of the Grzegorczyk hierarchy, it can be shown that every primitive recursive strictly decreasing infinite sequence of ordinals can be "slowed down" so that it can be transformed to a Goodstein sequence where bn = n + 1, thus giving an alternative proof to the same result Kirby and Paris proved.
The Goodstein sequence of a number can be effectively enumerated by a Turing machine; thus the function which maps n to the number of steps required for the Goodstein sequence of n to terminate is computable by a particular Turing machine.
Because every Goodstein sequence eventually terminates, this function is total.
But because Peano arithmetic does not prove that every Goodstein sequence terminates, Peano arithmetic does not prove that this Turing machine computes a total function.