Editing Goodstein's theorem (section)

== Proof of Goodstein's theorem ==

Goodstein's theorem can be proved (using techniques outside Peano arithmetic, see below) as follows: Given a Goodstein sequence <math>G_m</math>, we construct a parallel sequence <math>P_m</math> of [[ordinal number]]s in [[Cantor normal form]] which is strictly decreasing and terminates. A common misunderstanding of this proof is to believe that <math>G_m</math> goes to <math>0</math> ''because'' it is dominated by <math>P_m</math>. Actually, the fact that <math>P_m</math> dominates <math>G_m</math> plays no role at all. The important point is: <math>G_m(k)</math> exists if and only if <math>P_m(k)</math> exists (parallelism), and comparison between two members of <math>G_m</math> is preserved when comparing corresponding entries of <math>P_m</math>.{{sfn|Rathjen|2014|loc=lemma 2.2}} Then if <math>P_m</math> terminates, so does <math>G_m</math>. By [[infinite regress]], <math>G_m</math> must reach <math>0</math>, which guarantees termination.

We define a function <math>f=f(u,k)</math> which computes the hereditary base <math>k</math> representation of <math>u</math> and then replaces each occurrence of the base <math>k</math> with the first infinite [[ordinal number]] <math>\omega</math>. For example, <math>f(100,3)=f(3^{3^1+1}+2\cdot3^2+1,3)=\omega^{\omega^1+1} + \omega^2\cdot2 + 1 = \omega^{\omega+1} + \omega^2\cdot2 + 1</math>.

Each term <math>P_m(n)</math> of the sequence <math>P_m</math> is then defined as <math>f(G_m(n),n+1)</math>. For example, <math>G_3(1) = 3 = 2^1 + 2^0</math> and <math>P_3(1) = f(2^1 + 2^0,2) = \omega^1 + \omega^0 = \omega + 1</math>. Addition, multiplication and exponentiation of ordinal numbers are well defined.

We claim that <math>f(G_m(n),n+1) > f(G_m(n+1),n+2)</math>:

Let <math>G'_m(n)</math> be <math>G_m(n)</math> after applying the first, 
''base-changing'' operation in generating the next element of the Goodstein sequence, 
but before the second ''minus 1'' operation in this generation. 
Observe that <math>G_m(n+1)= G'_m(n)-1</math>.

Then <math>f(G_m(n),n+1) = f(G'_m(n),n+2)</math>. Now we apply the ''minus 1'' operation, and <math>f(G'_m(n),n+2) > f(G_m(n+1),n+2)</math>, as <math> G'_m(n) = G_m(n+1)+1</math>.
For example, <math>G_4(1)=2^2</math> and <math>G_4(2)=2\cdot 3^2 + 2\cdot 3+2</math>, so <math>f(2^2,2)=\omega^\omega</math> and <math>f(2\cdot 3^2 + 2\cdot 3+2,3)=
\omega^2\cdot2+\omega\cdot2+2</math>, which is strictly smaller. Note that in order to calculate <math>f(G_m(n),n+1)</math>, we first need to write 
<math>G_m(n)</math> in hereditary base <math>n+1</math> notation, as for instance the expression <math>\omega^\omega-1</math> is not an ordinal.

Thus the sequence <math>P_m</math> is strictly decreasing. 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). But <math>P_m(n)</math> is calculated directly from <math>G_m(n)</math>. Hence the sequence <math>G_m</math> must terminate as well, meaning that it must reach <math>0</math>.

While this proof of Goodstein's theorem is fairly easy, the ''Kirby–Paris theorem'',{{sfn|Kirby|Paris|1982}} which shows that Goodstein's theorem is not a theorem of Peano arithmetic, is technical and considerably more difficult. It makes use of [[Non-standard model of arithmetic|countable nonstandard models]] of Peano arithmetic.

=== Extended Goodstein's theorem ===
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 <math>b</math> with <math>b+2</math> instead of <math>b+1</math>.
More generally, let <math>b_1</math>, <math>b_2</math>, <math>b_3, \ldots</math> be any non-decreasing sequence of integers with <math>b_1 \geq 2</math>.
Then let the <math>(n+1)</math>st
term  <math>G_m(n+1)</math> of the extended Goodstein sequence of <math>m</math> be as
follows:
* Take the hereditary base <math>b_n</math> representation of <math>G_m(n)</math>.
* Replace each occurrence of the base <math>b_n</math> with <math>b_{n+1}</math>.
* Subtract one.
A simple modification of the above proof shows that this sequence still terminates. For example, if <math>b_n = 4</math> and if <math>b_{n+1} = 9</math>,
then <math>f(3 \cdot 4^{4^4} + 4, 4) = 3 \omega^{\omega^\omega} + \omega= f(3
\cdot 9^{9^9} + 9, 9)</math>, hence the ordinal <math>f(3 \cdot 4^{4^4} +
4, 4)</math> is strictly greater than the ordinal <math>f\big((3 \cdot
9^{9^9} + 9) - 1, 9\big).</math>

The extended version is in fact the one considered in Goodstein's original paper,{{sfn|Goodstein|1944}} where Goodstein proved that it is equivalent to the restricted ordinal theorem (i.e. the claim that [[transfinite induction]] below [[Epsilon numbers (mathematics)|ε<sub>0</sub>]] is valid), and gave a [[finitist]] proof for the case where <math>m \le b_1^{b_1^{b_1}}</math> (equivalent to transfinite induction up to <math>\omega^{\omega^\omega}</math>).

The extended Goodstein's theorem without any restriction on the sequence ''b<sub>n</sub>'' 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 ε<sub>0</sub>-induction.{{sfn|Rathjen|2014}} 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 ''b<sub>n</sub>'' to primitive recursive sequences would have allowed Goodstein to prove an unprovability result.{{sfn|Rathjen|2014}} 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 <math>b_n = n+1</math>, thus giving an alternative proof to the same result Kirby and Paris proved.{{sfn|Rathjen|2014}}