Goodstein’s Theorem Revisited

Abstract

Prompted by Gentzen’s 1936 consistency proof, Goodstein found a close fit between descending sequences of ordinals $<\varepsilon _{0}$ and sequences of integers, now known as Goodstein sequences. This chapter revisits Goodstein’s 1944 paper. In light of new historical details found in a correspondence between Bernays and Goodstein, we address the question of how close Goodstein came to proving an independence result for PA. We also present an elementary proof of the fact that already the termination of all special Goodstein sequences, i.e. those induced by the shift function, is not provable in PA. This was first proved by Kirby and Paris in 1982, using techniques from the model theory of arithmetic. The proof presented here arguably only uses tools that would have been available in the 1940s or 1950s. Thus we ponder the question whether striking independence results could have been proved much earlier? In the same vein we also wonder whether the search for strictly mathematical examples of an incompleteness in PA really attained its “holy grail” status before the late 1970s. Almost no direct moral is ever given; rather, the paper strives to lay out evidence for the reader to consider and have the reader form their own conclusions. However, in relation to independence results, we think that both Gentzen and Goodstein are deserving of more credit.

Appendix

It remains to prove Lemma 3.2. To this end the following is useful.

Lemma A.1

Recall that for a function $h: \mathbb{N} \rightarrow \mathbb{N}$ we defined h⁰(l) = l and $h^{k+1}(l) = h(h^{k}(l))$. Also recall that the hierarchy $(f_{l})_{l\in \mathbb{N}}$ is generated by the functions $f_{0}(n) = n + 1$ and $f_{l+1}(n) = (f_{l})^{n}(n)$. We shall write $f_{l}^{n}$ rather than $(f_{l})^{n}$.

Let f be any of the functions f _l in this hierarchy. Then f satisfies the following properties:

• (i) f(x) ≥ x + 1 if x > 0.

• (ii) f ^z (x) ≥ x for all x,z.

• (iii) If x < y then f(x) < f(y) and $f^{z}(x) <f^{z}(y)$ .

• (iv) $f_{l+1}(x) \geq f_{l}(x)$ whenever x > 0.

Proof

(i)–(iii) will be proved simultaneously by induction on l. (i) and (iii) are obvious for f = f ₀ and (ii) follows via a trivial induction on z. Now assume that (i)–(iii) hold for f _k and $l = k + 1$. For x > 0 one then computes

$$\displaystyle{f_{l}(x) = f_{k}^{x}(x) = f_{ k}(f_{k}^{x-1}(x)) \geq f_{ k}(x) \geq x + 1}$$

using the properties for f _k . (ii) follows from this by induction on z. As to (iii), note that

$$\displaystyle{f_{l}(x + 1) = f_{k}^{x+1}(x + 1) = f_{ k}(f_{k}^{x}(x + 1))> f_{ k}(f_{k}^{x}(x)) \geq f_{ k}^{x}(x) = f_{ l}(x),}$$

using the properties for f _k , and thus (iii) follows by straightforward inductions on y and z.

If x > 0, then $f_{l+1}(x) = f_{l}^{x}(x) = f_{l}(f_{l}^{x-1}(x)) \geq f_{l}(x)$ by (ii) and (iii). □ 

Proof of Lemma 3.2

We want to prove that for or every primitive recursive function h of arity r there is an n such $h(\vec{x}\,) \leq f_{n}(\max (2,\vec{x}\,))$ holds for all $\vec{x} = x_{1},\ldots,x_{r}$.

We show this by induction on the generation of the primitive recursive functions. Clearly for all n we have $h(\vec{x}) \leq f_{n}(\max (2,\vec{x}\,))$ by Lemma A.1(i) if h is any of the initial functions $x\mapsto 0$, $\vec{x}\mapsto x_{i}$, and $x\mapsto x + 1$.

Now let h be defined by $h(\vec{x}\,) = g(\varphi _{1}(\vec{x}\,),\ldots,\varphi _{s}(\vec{x}\,))$ and assume that the assertion holds for $g,\varphi _{1},\ldots,\varphi _{s}$. By Lemma 3.2(iv) we can then pick an n such that $g(\vec{y}\,) \leq f_{n}(\max (2,\vec{y}\,))$ and $\varphi _{i}(\vec{x}\,) \leq f_{n}(\max (2,\vec{y}\,))$ hold for all $\vec{y},\vec{x}$ and $1 \leq i \leq s$. As a result,

$$\displaystyle\begin{array}{rcl} h(\vec{x}\,)& \leq & f_{n}(\max (2,f_{n}(\max (2,\vec{x}\,)))) = f_{n}(f_{n}(\max (2,\vec{x}\,))) = {}\\ & & f_{n}^{2}(\max (2,\vec{x}\,)) \leq f_{ n}^{\max (2,\vec{x}\,)}(\max (2,\vec{x}\,)) = f_{ n+1}(\max (2,\vec{x}\,)), {}\\ \end{array}$$

showing that f _n+1 is a majorant for h.

Now suppose h is defined by primitive recursion from g and $\varphi$ via $h(\vec{x},0) = g(\vec{x}\,)$ and $h(\vec{x},y + 1) =\varphi (\vec{x},y,h(\vec{x},y))$ and that f _n majorizes g and $\varphi$, i.e. $g(\vec{x}\,) \leq f_{n}(\max (2,\vec{x}\,))$ and $\varphi (\vec{x},y,z) \leq f_{n}(\max (2,\vec{x}\,))$. We claim that

$$\displaystyle\begin{array}{rcl} h(\vec{x},y)& \leq & f_{n}(\max (2,\vec{x},y)).{}\end{array}$$

(7)

We prove this by induction on y. For y = 0 we have $h(\vec{x},y) = g(\vec{x}\,) \leq f_{n}(\max (2,\vec{x}\,)) = f_{n}^{1}(\max (2,\vec{x}\,))$. For the induction step we compute

$$\displaystyle\begin{array}{rcl} h(\vec{x},y + 1)& =& \varphi (\vec{x},y,h(\vec{x},y)) \leq f_{n}(\max (2,\vec{x},y,h(\vec{x},y))) {}\\ & \leq & f_{n}(\max (2,\vec{x},y,f_{n}^{y+1}(\max (2,\vec{x},y)))) = f_{ n}(f_{n}^{y+1}(\max (2,\vec{x},y))) {}\\ & =& f_{n}^{y+2}(\max (2,\vec{x},y)) {}\\ \end{array}$$

where the second “ ≤ ” uses the inductive assumption and the penultimate “ = ” uses Lemma A.1.

From the claim (7) we get with Lemma A.1, letting $w =\max (2,\vec{x},y)$, that

$$\displaystyle\begin{array}{rcl} h(\vec{x},y)& \leq & f_{n}^{y+1}(\max (2,\vec{x},y)) \leq f_{ n}^{w+1}(w) = f_{ n}(f_{n}^{w}(w)) = f_{ n}(f_{n+1}(w)) {}\\ & \leq & f_{n+1}(f_{n+1}(w)) = f_{n+1}^{2}(w) \leq f_{ n+1}^{w}(w) = f_{ n+2}(w). {}\\ \end{array}$$

As a result, $h(\vec{x},y) \leq f_{n+2}(\max (2,\vec{x},y))$. □