Goodstein sequence

A Goodstein sequence is a certain class of integer sequences Gk(n) that give rise to a quickly growing function that eventually dominates all recursive functions which are provably total in Peano arithmetic, but is itself provably total in PA + "\(\varepsilon_0\) is well-ordered".Weisstein, Eric W., Goodstein Sequence, MathWorld. Here, the additional axiom "\(\varepsilon_0\) is well-ordered" should be formulated in terms of the transfinite induction along an ordinal notation definable in PA but not provably well-founded in PA.
== Definition ==
Suppose we write a nonnegative integer n as a sum of powers of k, then we write the k exponents themselves as similar sums of powers, repeating this process until we get all topmost exponents less than k. For example, we can write 100 as + + = + + . We call this the base-k hereditary representation as n.
In the above representation of 100, we can "bump" the base 2 up by one, forming a different number + + . We write this larger number as B[2](100), and in general, B[b](n) means finding the base-b hereditary representation of n and bumping the base.
Now we define the recursive sequence G0(n) = n and Gk(n) = B[k + 1](Gk - 1(n)) - 1. In other words, as k increases, we are repeatedly bumping the base and subtracting one:
:G0(100) = 100 = + + 
:G1(100) = B[2](100) - 1 = + + - 1 = 228,767,924,549,636
:G2(100) = B[3](G1(100)) - 1 = + + 2 x + 2 x 4 + 2 x 1 - 1 = 3.486030062 x 
This rapidly growing sequence is known as a Goodstein sequence. Surprisingly, for all values of n, Gk(n) eventually peaks, declines, and returns to zero. This fact is known as Goodstein's theorem. Even more surprisingly, it can be shown that Goodstein's theorem cannot be proved in Peano arithmetic.
== Unprovability ==
Let G(n) be the number of steps it takes for the Goodstein sequence starting with n to terminate (i.e. reach zero). Formally, G(n) as the smallest k for which Gk(n) = 0. G(n) is an extremely fast-growing function. Note that some authors define G(n) as the length of the Goodstein sequence starting with n, which increases the outputs of the function by 1 because in this case the first step (G0(n)) is included.
Define \(R^\omega_b (n)\) to be the ordinal obtained by writing n in base-b hereditary notation, then replacing every instance of b by \(\omega\), for instance
\[R^\omega_2 (100) = R^\omega_2 (2^{2^2 + 2} + 2^{2^2 + 1} + 2^2) = \omega^{\omega^\omega + \omega} + \omega^{\omega^\omega + 1} + \omega^\omega\]
Then \(G(n) = H_{R^\omega_2 (n)} (3) - 3\) in the Hardy hierarchy, which shows that \(G(2 \uparrow\uparrow n)\) is \(H_{\varepsilon_0} (n)-3\). So, it grows as fast as Jonathan Bowers' tetrational arrays. Since this function grows faster than any function provably recursive in Peano arithmetic, Goodstein's theorem is not provable in Peano arithmetic. 
== Values and bounds of \(G(n)\) ==
=== Notes ===
* \(^ba\) indicates tetration.
* \(\uparrow\) indicates arrow notation.
* \(Ack(n)\) indicates unary Ackermann function (Friedman's version).
* \(\lbrace\rbrace\) indicates BEAF.
* \(f_\alpha(n)\) indicates FGH.
n 	Lower bound 	G(n) 	Upper bound
0 	0 	0 	0
1 	1 	1 	1
2 	3 	3 	3
3 	5 	5 	5
4 	\(f_3(3)-3 = 3\cdot2^{402,653,211}-3\) 	\(f_3(3)-3 = 3\cdot2^{402,653,211}-3\) 	\(f_3(3)-3 = 3\cdot2^{402,653,211}-3\)
5 	\((10\uparrow\uparrow (10 \uparrow\uparrow (10 \uparrow\uparrow 10^{10^{10^{20}}}))\) 	\(f_4(4)-3\) 	\(4 \uparrow\uparrow\uparrow 8\)
6 	\((10\uparrow^4)^5 (10\uparrow\uparrow\uparrow)^5 (10\uparrow\uparrow)^5 (10 \uparrow)^5 117\) 	\(f_6(6)-3\) 	\(6 \uparrow^5 12\)
7 	\((10 \uparrow^6)^7 (10\uparrow^5)^7 (10 \uparrow^4)^7 (10\uparrow\uparrow\uparrow)^7 (10 \uparrow\uparrow)^7 (10 \uparrow)^7 619\)	\(f_8(8)-3\) 	\(8 \uparrow^7 16\)
8 	\(Ack (Ack (3 \times 2^{402,653,211})) \) 	\(f_{\omega+1}(3)-3\) 	\(\lbrace 3,4,1,2 \rbrace\)
9 	\(Ack (Ack (Ack (G(5))))\) 	\(f_{\omega+1}(4)-3\) 	\(\lbrace 4,5,1,2 \rbrace\)
10 	\(Ack^5 (G(6))\) 	\(f_{\omega+1}(6)-3\) 	\(\lbrace 6,7,1,2 \rbrace\)
11 	\(Ack^7 (G(7))\) 	\(f_{\omega+1}(8)-3\) 	\(\lbrace 8,9,1,2 \rbrace\)
12 	\(Ack^{3 \times 2^{402,653,211}}(3 \times 2^{402,653,211})\) 	\(f_{\omega+1}(f_3(3))-3\) 	\(\lbrace G(4),G(4)+1,1,2 \rbrace\)
13 	\(Ack^{G(5)}(G(5))\) 	\(f_{\omega+1}(f_4(4))-3\) 	\(\lbrace G(5),G(5)+1,1,2 \rbrace\)
14 	\(Ack^{G(6)}(G(6))\) 	\(f_{\omega+1}(f_6(6))-3\) 	\(\lbrace G(6),G(6)+1,1,2 \rbrace\)
15 	\(Ack^{G(7)}(G(7))\) 	\(f_{\omega+1}(f_8(8))-3\) 	\(\lbrace G(7),G(7)+1,1,2 \rbrace\)
16 	\(\lbrace 3,4,3,3,3 \rbrace\) 	\(f_{\omega^3}(3)-3\) 	\(\lbrace 3,5,3,3,3 \rbrace\)
17 	\(\lbrace 4,5,4,4,4,4 \rbrace\) 	\(f_{\omega^4}(4)-3\) 	\(\lbrace 4,6,4,4,4,4 \rbrace\)
18 	\(\lbrace 6,7,6,6,6,6,6,6 \rbrace\) 	\(f_{\omega^6}(6)-3\) 	\(\lbrace 6,8,6,6,6,6,6,6 \rbrace\)
19 	\(\lbrace 8,9,8,8,8,8,8,8,8,8 \rbrace\) 	\(f_{\omega^8}(8)-3\) 	\(\lbrace 8,10,8,8,8,8,8,8,8,8 \rbrace\)
20 	\(\lbrace G(4),G(4)+2 (1) 2 \rbrace\) 	\(f_{\omega^\omega}(f_3(3))-3\) 	\(\lbrace G(4),G(4)+3 (1) 2 \rbrace\)
32 	\(\lbrace 3,4,2 (1) 2 \rbrace\) 	\(f_{\omega^\omega+1}(3)-3\) 	\(\lbrace 3,5,2 (1) 2 \rbrace\)
64 	\(\lbrace 3,4,4 (1) 2 \rbrace\) 	\(f_{\omega^\omega+3}(3)-3\) 	\(\lbrace 3,5,4 (1) 2 \rbrace\)
128 	\(\lbrace 3,4,1,2 (1) 2 \rbrace\) 	\(f_{\omega^\omega+\omega+1}(3)-3\) 	\(\lbrace 3,5,1,2 (1) 2 \rbrace\)
256 	\(\lbrace 3,5 (1) 3 \rbrace\) 	\(f_{(\omega^\omega)3}(3)-3\) 	\(\lbrace 3,6 (1) 3 \rbrace\)
65,536 	\(\lbrace 3,3 (3) 2 \rbrace\) 	\(f_{\omega^{\omega^3}}(3)-3\) 	\(\lbrace 3,4 (3) 2 \rbrace\)
65,540 	\(\lbrace 3,3 (G(4)) 2 \rbrace\) 	\(f_{\omega^{\omega^\omega}}(f_3(3))-3\) 	\(\lbrace 3,3 (G(4)+1) 2 \rbrace\)
\(2^{65,536}\) 	\(\lbrace 3,3 (3,3,3,2) 3 \rbrace\) 	\(f_{\omega^{\omega^{\omega^3}}}(3)-3\) 	\(\lbrace 3,4 ((1) 2) 2 \rbrace\)
\(2^{65,536}+4\)	\(\lbrace 3,G(4) ((1) 2) 2 \rbrace\) 	\(f_{\omega^{\omega^{\omega^\omega}}}(f_3(3))-3\)	\(\lbrace 3,G(4)+1 ((1) 2) 2 \rbrace\)
\(^n2\) 	\(^{n-2}3 \& 3\) 	\(f_{^{n-1}\omega}(3)-3\) 	\(^{n-1}3 \& 3\)
== Weak Goodstein function ==
If we use the ordinary base representation instead of the hereditary representation, Goodstein's theorem still holds. The sequences in this system are called weak Goodstein sequences, producing the weak Goodstein function \(g(n)\).
Like its stronger cousin, \(g(n)\) can be computed using the Hardy hierarchy, putting it on par with \(f_{\omega}(n)\) in the fast-growing hierarchy, or about \(2 \uparrow^{n-1} n\) in arrow notation.
n 	Lower bound for g(n) 	Upper bound for g(n)
0 	0 	0
1 	1 	1
2 	3 	3
3 	5 	5
4 	21 	21
5 	61 	61
6 	381 	381
7 	2045 	2045
8 	\(3 \times 2^{402,653,211}-3\) 	\(3 \times 2^{402,653,211}-3\)
9 	\(10^{10^{3.5539 \times 10^{20}}}\) 	\(10^{10^{3.5540 \times 10^{20}}}\)
10 	\(10^{10^{10^{10^{4.5546 \times 10^{117}}}}}\) 	\(10^{10^{10^{10^{4.5547 \times 10^{117}}}}}\)
11 	\(10^{10^{10^{10^{10^{10^{1.9923 \times 10^{619}}}}}}}\)	\(10^{10^{10^{10^{10^{10^{1.9924 \times 10^{619}}}}}}}\)
12 	\(10 \uparrow\uparrow 24\) 	\(10 \uparrow\uparrow 25\)
13 	\(10 \uparrow\uparrow 65\) 	\(10 \uparrow\uparrow 66\)
14 	\(10 \uparrow\uparrow 385\) 	\(10 \uparrow\uparrow 386\)
15 	\(10 \uparrow\uparrow 2,049\) 	\(10 \uparrow\uparrow 2,050\)
16 	\((10 \uparrow\uparrow)^{2} (g(4)+2)\) 	\((10 \uparrow\uparrow)^{2} (g(4)+3)\)
17 	\((10 \uparrow\uparrow)^{3} (g(5)+2)\) 	\((10 \uparrow\uparrow)^{3} (g(5)+3)\)
18 	\((10 \uparrow\uparrow)^{5} (g(6)+2)\) 	\((10 \uparrow\uparrow)^{5} (g(6)+3)\)
19 	\((10 \uparrow\uparrow)^{7} (g(7)+2)\) 	\((10 \uparrow\uparrow)^{7} (g(7)+3)\)
20 	\(10 \uparrow\uparrow\uparrow 24\) 	\(10 \uparrow\uparrow\uparrow 25\)
32 	\((10 \uparrow\uparrow\uparrow)^{3} (g(8)+3)\) 	\((10 \uparrow\uparrow\uparrow)^{3} (g(8)+4)\)
64 	\((10 \uparrow\uparrow\uparrow\uparrow)^{3} (g(16)+3)\) 	\((10 \uparrow\uparrow\uparrow\uparrow)^{3} (g(16)+4)\)
\(2^n\)	\(2 \uparrow^{n-1} n\) 	\(2 \uparrow^n n\)
== External links ==
*Justin T Miller, Some elements of a proof that Goodstein's theorem is not a theorem of PA, undergraduate thesis.
*Dan Kaplan, A Classification of non stanard models of Peano Arithmetic by Goodstein's theorem, Thesis in Franklan and Marshall College Library
*Definitions of Goodstein sequences in the programming languages Ruby and Haskell, as well as a large-scale plot
*Goodstein Sequences: The Power of a Detour via Infinity - good exposition with illustrations of Goodstein Sequences and the hydra game.
== Sources ==
ja:グッドスタイン数列
fr:Suite de Goodstein
Category:Functions
Category:Theorems
Category:Sequences