Which part(s) of this proof of Goodstein's Theorem are not expressible in Peano arithmetic?

Question

EDIT: Noah Schweber helpfully points out that $\mathsf{ACA}_0$ is a conservative extension of Peano arithmetic in which certain aspects of my proof not expressible in Peano arithmetic are expressible. So perhaps my question should focus on which part(s) of the proof below are not expressible in $\mathsf{ACA}_0$ [or perhaps substitute instead whatever your favourite conservative extension of $\mathsf{PA}$ happens to be].

---

[In this post, $\mathbb{N}$ includes $0$.]

I know that Goodstein's Theorem is not provable within Peano arithmetic. But I think I can express the proof of Goodstein's Theorem in a way that feels like it consists entirely of "explicitly constructive" reasoning about natural numbers.

So then, not really knowing anything about formal logic, the question that naturally arises for me is: Which part(s) of the proof below are not expressible in Peano arithmetic?

Lexicographical order

Definition 1. Given non-empty finite totally ordered sets \begin{align*} S &= \{s_1 < \ldots < s_N \} \\ T &= \{t_1 < \ldots < t_M \}, \end{align*} we define the lexicographical order on the set $\,T^S\,$ of functions from $S$ to $T$ by specifying that $f<g$ if and only if there exists $i \in \{1,\ldots,N\}$ such that

• every integer $j$ with $i < j \leq N$ has $f(s_j)=g(s_j)$;
• $f(s_i) < g(s_i)$.

(It is not hard to show that the lexicographical order on $T^S$ is a total order.)

A representation of hereditary base-$m$ expressions

Recursive Definition 2. For each integer $m \geq 2$:

• Let $S_{0,m}$ be a singleton, equipped with its unique total order.
• For each integer $k \geq 1$, let $\,S_{k,m}=\{0,\ldots,m-1\}^{S_{k-1,m}}$, equipped with the lexicographical order.

For convenience, we will from now on assume that $S_{0,m}=\{\emptyset\}$.

Recursive Definition 3. For each integer $m \geq 2$:

• Define $F_{0,m} \colon S_{0,m} \to \mathbb{N}$ by $F_{0,m}(\emptyset)=0$.
• For each integer $k \geq 1$, define $F_{k,m} \colon S_{k,m} \to \mathbb{N}$ by $$ F_{k,m}(f) = \sum_{h \in S_{k-1,m}} f(h)m^{F_{k-1,m}(h)} $$

Lemma 4. For each integer $m \geq 2$ and each integer $k \geq 1$, $F_{k,m}$ serves as an order-isomorphism from $S_{k,m}$ to $\{0,\ldots,(m\uparrow\uparrow k) - 1\}$.

Proof. Fix $m$. For $k=1$ the result follows immediately from the fact that $m^0=1$. Assuming the result for $k=k_0-1$ (where $k_0 \geq 2$), the result for $k=k_0$ then follows from the fact that the set of base-$m$ expressions of length $N_0:=m\uparrow\uparrow (k_0-1)$ is order-isomorphically mapped by evaluation onto $\{0,\ldots,m^{N_0} - 1\}$. $\quad\square$

Natural embedding of hereditary expressions

Recursive Definition 5. For each integer $m \geq 2$:

• Let $\iota_{0,m}$ be the unique function from $S_{0,m}$ to $S_{0,m+1}$.
• For each integer $k \geq 1$, define the injective function $\,\iota_{k,m} \colon S_{k,m} \to S_{k,m+1}$ by $$ \iota_{k,m}(f)(h) = \begin{cases} f(\iota_{k-1,m}^{-1}(h)) & \text{if } h \in \iota_{k-1,m}[S_{k-1,m}] \\ 0 & \text{if } h \not\in \iota_{k-1,m}[S_{k-1,m}] \end{cases} \qquad \forall \ f \in S_{k,m} \, , \, h \in S_{k-1,m+1}. $$ [This is injective because, for any $f,g \in S_{k,m}$ that disagree at a point $\tilde{h} \in S_{k-1,m}$, we have that $\iota_{k,m}(f)$ and $\iota_{k,m}(g)$ disagree at $\iota_{k-1,m}(\tilde{h})$.]

Lemma 6. For each integer $m \geq 2$ and each integer $k \geq 0$, $\iota_{k,m} \colon S_{k,m} \to S_{k,m+1}$ is an order-embedding.

Proof. Fixing $m$, the result is a straightforward induction in $k$. $\quad\square$

Definition 7. For integers $m_2 > m_1 \geq 2$ and $k \geq 0$, define $\,\iota_{k,m_1,m_2} \colon S_{k,m_1} \to S_{k,m_2}\,$ by $$ \iota_{k,m_1,m_2} = \iota_{k,m_2-1} \circ \ldots \circ \iota_{k,m_1} $$

Decreasing sequences of hereditary expressions

For each integer $k \geq 0$, let $S_k = \bigcup_{m=2}^\infty S_{k,m}$.

Definition 8. Given an integer $k \geq 0$, a $k$-sequence is a function $\alpha \colon I \to S_k$ for which $I$ is an infinite subset of $\{2,3,4,\ldots\}$ and every $m \in I$ has $\alpha(m) \in S_{k,m}$.

Definition 9. Given an integer $k \geq 0$, a $k$-sequence $\alpha \colon I \to S_k$ is called decreasing if for all $m_1,m_2 \in I$ with $m_1 < m_2$, we have $$ \alpha(m_2) < \iota_{k,m_1,m_2}(\alpha(m_1)). $$

The strategy in proof of Goodstein's Theorem will be to construct a way of getting from a decreasing $k$-sequence to a decreasing $(k-1)$-sequence; this ultimately leads down to a decreasing $1$-sequence, which will result in a contradiction.

A basic lemma about embedding of lexicographical order

Lemma 10. For integers $m_2 > m_1 \geq 2$ and $k \geq 1$, if we have $f_1 \in S_{k,m_1}$ and $f_2 \in S_{k,m_2}$ such that $$ f_2 < \iota_{k,m_1,m_2}(f_1), $$ then: (A) the set $$ H(f_1,f_2) := \{ h \in S_{k-1,m_1} \, : \, f_2(\iota_{k-1,m_1,m_2}(h)) < f_1(h) \} $$ is non-empty; (B) letting $h_\ast = \max H(f_1,f_2)$, we have

• for all $h \in S_{k-1,m_1}$ with $h>h_\ast$, $\,f_2(\iota_{k-1,m_1,m_2}(h)) = f_1(h)$;
• for all $h \in S_{k-1,m_2} \setminus \iota_{k-1,m_1,m_2}[S_{k-1,m_1}]$ with $h > \iota_{k-1,m_1,m_2}(h_\ast)$, $\,f_2(h)=0$.

Proof. (A) If $H(f_1,f_2)$ is empty then we have that for every $h \in S_{k-1,m_2}$, $$ f_2(h) \geq \iota_{k,m_1,m_2}(f_1)(h), $$ contradicting that $f_2 < \iota_{k,m_1,m_2}(f_1)$. (B) By definition, every $h \in S_{k-1,m_1}$ with $h>h_\ast$ has $\,f_2(\iota_{k-1,m_1,m_2}(h)) \geq f_1(h)$. So, since $\iota_{k-1,m_1,m_2}$ is order-preserving, it follows that for every $h \in S_{k-1,m_2}$ with $h>\iota_{k-1,m_1,m_2}(h_\ast)$, $f_2(h) \geq \iota_{k,m_1,m_2}(f_1)(h)$. Since $f_2 < \iota_{k,m_1,m_2}(f_1)$, it then follows that for every $h \in S_{k-1,m_2}$ with $h>\iota_{k-1,m_1,m_2}(h_\ast)$, $f_2(h) = \iota_{k,m_1,m_2}(f_1)(h)$, giving the result. $\quad\square$

Proof of Goodstein's Theorem

Suppose for a contradiction that we have an integer $p \geq 1$ such that the Goodstein sequence starting at $p$ does not terminate. Let $k \geq 1$ be an integer such that $p<2\uparrow\uparrow k$. Due to Lemma 4, a simple recursion enables us to construct a decreasing $k$-sequence $\alpha \colon \{2,3,4,\ldots\} \to S_k$ such that the Goodstein sequence is given by $\big( F_{k,m}(\alpha(m)) \big)_{\!m \geq 2}$.

We now recursively construct a finite list $$ ( \ \ \alpha_0 \colon I_0 \to S_k \quad , \quad \alpha_1 \colon I_1 \to S_{k-1} \quad , \quad \ldots \quad , \quad \alpha_N \colon I_N \to S_{k-N} \ \ ) $$ for some $N \leq k$, where for each $j \in \{0,\ldots,N\}$, $\alpha_j$ is a $(k-j)$-sequence, as follows:

Firstly, $I_0=\{2,3,4,\ldots\}$ and $\alpha_0=\alpha$.

Now for each integer $j \in \{0,\ldots,k\}$ for which $(\alpha_0,\ldots,\alpha_j)$ exists, do the following procedure:

If $j=k$, or if $j<k$ and $\alpha_j$ is not decreasing, then take $N=j$.

If $j<k$ and $\alpha_j$ is decreasing, then recursively define sequences $(m_{j,n})_{n \in \mathbb{N}}$ and $(h_{j,n})_{n \in \mathbb{N}}$ by

• $m_{j,0} = \min I_j\,$,
• for each integer $n \geq 0$, writing \begin{align*} H_{j,n} :=& \bigcup_{\substack{m \in I_j \\ m > m_{j,n}}} H(\alpha_j(m_{j,n}) \, , \, \alpha_j(m)) \\ =& \ \{ h \in S_{k-j-1,m_{j,n}} \, : \, \exists \, m \in I_j \text{ with } m > m_{j,n} \text{ s.t. } \alpha_j(m)(\iota_{k-j-1,m_{j,n},m}(h)) < \alpha_j(m_{j,n})(h) \} \end{align*} [which is non-empty by Lemma 10(A)], let $$ h_{j,n} = \max \, H_{j,n} \, , $$ and writing $$ x_{j,n} := \min\{ \alpha_j(m)(\iota_{k-j-1,m_{j,n},m}(h_{j,n})) \, : \, m \in I_j \text{ with } m > m_{j,n} \}, $$ let $$ m_{j,n+1} = \min\{ m \in I_j \text{ with } m > m_{j,n} \, : \, \alpha_j(m)(\iota_{k-j-1,m_{j,n},m}(h_{j,n})) = x_{j,n} \} $$

and define $I_{j+1}=\{m_{j,n} : n \in \mathbb{N}\}$ and \begin{align*} &\alpha_{j+1} \,\colon\, I_{j+1} \to S_{k-j-1} \\ &\alpha_{j+1}(m_{j,n}) = h_{j,n}. \end{align*}

If $N=k$ then we have in particular that $\alpha_{k-1}$ is a decreasing $1$-sequence; so, for each integer $n \geq 1$, letting $m_n$ denote the $n$-th value in $I_{k-1}$ and letting $y_n=\alpha_{k-1}(m_n)(\emptyset)$, the sequence $(y_n)_{n \geq 1}$ is a strictly decreasing sequence of natural numbers. But then there is no possible value for the $(y_1+2)$-th term in this sequence, and so we have a contradiction.

So to complete the proof, it only remains to show that $N=k$, which we will do by induction. The base step is to show that $N>0$: this is immediate from the facts that $0<k$ and $\alpha$ is decreasing.

Now suppose we have an integer $j_0$ with $0 \leq j_0 \leq k-2$ such that $N>j_0$; we need to show that $N>j_0+1$. For this it is sufficient to show that $\alpha_{j_0+1}$ is decreasing. To do this, it is sufficient just to verify Definition 9 for consecutive pairs of integers in $I_{j_0+1}$, since then (due to transitivity of $<$) a simple induction argument will give that $\alpha_{j_0+1}$ satisfies Definition 9 in full. Consecutive pairs of integers in $I_{j_0+1}$ take the form $(m_{j_0,n} \, , \, m_{j_0,n+1})$ for some $n \in \mathbb{N}$.

So we need to show that for every $n \in \mathbb{N}$, $$ h_{j_0,n+1} < \iota_{k-j_0-1,m_{j_0,n},m_{j_0,n+1}}(h_{j_0,n}). $$ Fix any $n \in \mathbb{N}$. For convenience, let $\bar{\iota}=\iota_{k-j_0-1,m_{j_0,n},m_{j_0,n+1}}$; so we need to show that $h_{j_0,n+1} < \bar{\iota}(h_{j_0,n})$. Since $h_{j_0,n+1}$ is defined as the maximum of $H_{j_0,n+1}$, we need to show that every $h \in S_{k-j_0-1,m_{j_0,n+1}}$ with $h \geq \bar{\iota}(h_{j_0,n})$ lies outside of $H_{j_0,n+1}$. We split into the following three cases:

1. $h>\bar{\iota}(h_{j_0,n})$ and $h \in \bar{\iota}[S_{k-j_0-1,m_{j_0,n}}]$;
2. $h>\bar{\iota}(h_{j_0,n})$ and $h \not\in \bar{\iota}[S_{k-j_0-1,m_{j_0,n}}]$;
3. $h=\bar{\iota}(h_{j_0,n})$.

Case 1: Let $h'=\bar{\iota}^{-1}(h)$. For any $m \in I_{j_0}$ with $m>m_{j_0,n+1}$, Lemma 10(B) applied to both the pair $\big(\alpha_{j_0}(m_{j_0,n}) \, , \, \alpha_{j_0}(m_{j_0,n+1})\big)$ and the pair $\big(\alpha_{j_0}(m_{j_0,n}) \, , \, \alpha_{j_0}(m)\big)$ gives that $$ \alpha_{j_0}(m)(\iota_{k-j_0-1,m_{j_0,n+1},m}(h)) = \alpha_{j_0}(m_{j_0,n})(h') = \alpha_{j_0}(m_{j_0,n+1})(h). $$ Hence $h \not\in H_{j_0,n+1}$.

Case 2: For any $m \in I_{j_0}$ with $m>m_{j_0,n+1}$, Lemma 10(B) applied to both the pair $\big(\alpha_{j_0}(m_{j_0,n}) \, , \, \alpha_{j_0}(m_{j_0,n+1})\big)$ and the pair $\big(\alpha_{j_0}(m_{j_0,n}) \, , \, \alpha_{j_0}(m)\big)$ gives that $$ \alpha_{j_0}(m)(\iota_{k-j_0-1,m_{j_0,n+1},m}(h)) = 0 = \alpha_{j_0}(m_{j_0,n+1})(h). $$ Hence $h \not\in H_{j_0,n+1}$.

Case 3: For any $m \in I_{j_0}$ with $m>m_{j_0,n+1}$, we have $$ \alpha_{j_0}(m)(\iota_{k-j_0-1,m_{j_0,n+1},m}(h)) \geq x_{j_0,n} = \alpha_{j_0}(m_{j_0,n+1})(h). $$ Hence $h \not\in H_{j_0,n+1}$.

So we are done.

Answer 1

Because your argument involves arithmetical classes at several points, as you noticed, it is not directly expressible in the first-order language of $\newcommand\PA{\text{PA}}\PA$, although as Noah mentioned in the comments it is naturally expressible in the language of second-order arithmetic, which allows for both numbers and sets (classes) of numbers.

The theory $\newcommand\ACA{\text{ACA}}\ACA_0$ ensures the existence of all arithmetically definable sets of numbers, and is conservative over $\newcommand\PA{\text{PA}}\PA$. And many of the sets of numbers that you want to prove exist are indeed arithmetically definable, and thus would exist in $\ACA_0$.

However, it seems to me that you are also defining classes by recursion. For example, in the center of your argument you define the classes $I_j$ by recursion, as Sridhar Ramesh mentioned in the comments. In general, this is not possible even in $\ACA_0$, but requires the stronger theory $\newcommand\ATR{\text{ATR}}\ATR_0$, which allows for arithmetic recursions of that sort.

Consider for example the Tarskian recursive definition of truth, which is a simple arithmetic recursion on formulas — we define truth on the atomic formulas, and then explain how truth propogates through Boolean connectives and quantifiers. This is all arithmetically expressible, to define how truth extends from simpler formulas to the next level of complexity. But $\ACA_0$ does not prove that there is a truth predicate for arithmetic truth, in light of Tarski's theorem on the nondefinability of truth. Namely, there can be no arithmetically definable truth predicate for arithmetic truth. And therefore we cannot in general undertake arithmetical class recursions in $\ACA_0$.

It will not help you to argue that you require only a standard finite $k$ many steps in your recursion. That may be true, for any standard finite $p$, but however, we are discussing proving the Goodstein theorem, which is the universal claim about all $p$, not just each case separately. So you don't really know that $p$ is standard in the general case and therefore you can't know that $k$ is standard either.

But it can be undertaken in $\ATR_0$. This theory, however, is not conservative over $\ACA_0$, and implies $\text{Con}(PA)$ and so on. Your recursion is merely length $\omega$, which is a fragment of $\ATR_0$, but this is the same fragment used to define the truth predicate, so it also is not conservative.

Disclaimer: I haven't actually gone through all the details of your original post, and so please forgive me if I have misunderstood.