Could Kronecker accept a proof of Goodstein's theorem?

As a starting point, I recommend that you study the proof of Theorem 1 in my expository article on The Consistency of Arithmetic. (This is not exactly a proof of Goodstein's theorem, but for the purposes of the present discussion I think it's close enough. Start reading on page 25 where it says "Ordinals below $epsilon_0$.")

I have tried to make this proof as "pedestrian" as possible, avoiding concepts from logic and set theory that might be unfamiliar to the "working mathematician." In particular, my contention is that if you were to present this proof in (say) an undergraduate analysis class, it would seem completely unobjectionable and unremarkable. True, the proof assumes that it is meaningful to talk about infinite sequences, but infinite sequences are routinely bandied about in undergraduate analysis without comment. Also, the induction argument is trickier than most induction arguments, but I don't think that anyone would find anything suspicious about it unless they had been specifically told to look for something suspicious.

Sometimes the terms "PA proof" and "elementary proof" are used interchangeably. I think that this practice can lead to confusion. The class of proofs that are formalizable in PA is of course a very clearly defined class, but it does not correspond very closely to what we intuitively think of as "elementary" proofs. In particular, the $epsilon_0$ upper bound is, from the point of view of ordinary mathematical practice, a rather artificial bound. For example, we know from reverse mathematics that in a certain precise sense, the Bolzano–Weierstrass theorem goes beyond PA, but in our undergraduate analysis classes we don't set out flares or start blaring emergency sirens when proving Bolzano–Weierstrass. The exact logical strength of various assumptions that are used in ordinary mathematics is something that is not apparent on the surface, and emerges only after a careful logical analysis.

Conversely, it's possible to encode highly sophisticated concepts and proofs in PA—concepts that most mathematicians would instinctively regard as being "not at all elementary." EDIT (in light of the comments): For example, sometimes people ask if Fermat's Last Theorem can be proved in PA. I think that most of them are implicitly trying to ask whether there is an elementary proof of FLT. But as Angus Macintyre has shown (see comments below), it is very likely that all the high-falutin' super-fancy "non-elementary" machinery used in the known proof of FLT can be sufficiently well approximated in PA to push the proof through. If Macintyre is right, which I think he is, then this would show that FLT is provable in PA, while leaving completely unanswered the question of whether there is an "elementary" proof of FLT.

Returning to the question of Gauss or Kronecker, it's a little tough to guess what they would have thought about these things. They might have affirmed that they believed in "potential infinity" and not "actual infinity," but most modern mathematicians regard these two terms as philosophical gobbledygook, making it hard to translate Gauss's beliefs directly into present-day terms. We can probably safely say that they would have balked at ZFC, in particular the axiom of infinity, but the axiom of infinity isn't absolutely necessary for Goodstein's theorem. Indeed, Gentzen, in his proof of the consistency of PA, made an effort to argue that the reasoning was "finitary." Since "finitary" isn't a completely precise term either, it's hard to be sure that Gauss would have agreed with Gentzen, but it's at least plausible that he would have. Ultimately, like all historical counterfactuals, it's a matter of speculation what Gauss would have thought. But hopefully I've convinced you that there isn't anything more mysterious about Goodstein's theorem than many other routine mathematical theorems.

This is really an expansion of Aaron Bergman and others' comments as well as information that exists on the Wikipedia articles on Goodstein's theorem and epsilon numbers. I will sketch a proof of Goodstein's theorem and you'll have to tell me if Kronecker would have accepted it as a legitimate argument. (I'm not sure if this is the best 'elementary looking' proof and I don't know if this would be considered a long proof. If somebody knows a simpler proof that looks elementary please tell me. I'm also not sure how constructive this argument can be. As written it certainly isn't.)

Let $T$ be the collection of finite rooted trees. For each natural number $n$, let $T_n subset T$ be the collection of rooted finite trees of height at most $n$ (we'll say that the rooted tree with a single node has height $0$).

We will define a linear order $sqsubset$ on $T$ inductively by defining it on each $T_n$. $T_0$ has a single element, so the order on $T_0$ is the trivial order. Now for any $n$, given the order on $T_n$, for any $a in T_{n+1}$ we can associate a finite sequence of elements of $T_n$, which we'll write $s(a)$, by listing the children of the root note of $a$ in descending order according to $sqsubset$ (which we have already defined). Given $a,b in T_{n+1}$, we say that $asqsubset b$ if $aneq b$ and at the first index $i$ at which $s(a)$ and $s(b)$ differ, either $s(a)(i)$ doesn't exist or it does and $s(a)(i) sqsubset s(b)(i)$.

It is not hard to show that $sqsubset$ is a linear order on $T_{n+1}$, that $sqsubset$ as defined in $T_{n+1}$ agrees with $sqsubset$ as defined on $T_n$, and that $T_n$ is an initial segment of $T_{n+1}$ under $sqsubset$. Therefore we can treat $sqsubset$ as a linear order on all of $T$. Note that while $T$ is an infinite set, the elements of $T$ are finite objects (and can be coded by natural numbers) and the relation $asqsubset b$ is computable.

Lemma. For any $n$, if $f : mathbb{N} rightarrow T_n$ is non-increasing under $sqsubset$, then it is eventually constant.

Proof. We will show this by induction on $n$. The proposition is obvious for $n=0$. Assume that we've shown it for $T_{n}$ and let $f : mathbb{N} rightarrow T_{n+1}$ be a non-increasing function. Clearly if $f(k)$ is ever the unique element of $T_0$, then we're done, so assume that $f(k)$ is never in $T_0$.

Claim: For every $i in mathbb{N}$, the partial function $k mapsto s(f(k))(i)$ is eventually constant (i.e. either eventually always defined and a constant value or eventually always undefined).

Proof of claim. We will prove this by induction on $i$. For $i = 0$, we have that $k mapsto s(f(k))(0)$ is a non-increasing function whose codomain is $T_n$. By the overall induction hypothesis (on $n$), this implies that $k mapsto s(f(k))(0)$ is eventually constant.

Assume that we've shown the claim for some $i$ and consider the partial function $k mapsto s(f(k))(i+1)$. If $k mapsto s(f(k))(i)$ is eventually always undefined, then $k mapsto s(f(k))(i+1)$ is also eventually always undefined and we're done, so assume that $k mapsto s(f(k))(i)$ is eventually always defined and let it be constant on inputs larger than $m$. Consider $k mapsto s(f(m + k))(i+1)$. If this is ever undefined, then it is undefined for any larger inputs as well, so assume that it is always defined. In this case, we have that this is a non-increasing function from $mathbb{N}$ to $T_n$, so by the overall induction hypothesis we have that it must eventually be constant as well. So in both cases it is eventually constant.

Therefore by induction, $k mapsto s(f(k))(i)$ is eventually constant for every $i in mathbb{N}$, as required. $square_{text{claim}}$

For each $i$, let $g(i)$ be the eventual value of the map $k mapsto s(f(k))(i)$ (where we take $g(i)$ to be undefined if $s(f(k))(i)$ is undefined for sufficiently large $k$). We have that $g(i)$ is defined on an initial segment of the natural numbers, possibly all of them. Furthermore, since $s(a)$ is always in decreasing order, we have that $g(i)$ is a non-increasing partial function from $mathbb{N}$ to $T_n$. This means that if $g(i)$ is defined for all $i$, by the induction hypothesis we have that it is eventually constant.

Assume for the sake of contradiction that $g(i)$ is defined for all $i$. Let $a$ be its eventual value and let $j$ be some index such that $g(j) = a$. Choose $m$ such that for all $k in mathbb{N}$, $s(f(m+k))(j) = a$. Since $k mapsto s(f(m+k))(j)$ is constant, we have that $kmapsto s(f(m+k))(j+1)$ is non-increasing, and in particular must be defined for all $k$, otherwise $g(j+1)$ would be undefined. By construction we have that $s(f(m))(j+1) leq s(f(m))(j)$, so since the eventual value of $k mapsto s(f(m))(j+1)$ is also $a$, we must actually have $s(f(m+k))(j+1) = a$ for all $k in mathbb{N}$. Iterating this argument shows by induction that for any $ell geq j$, $s(f(m+k))(ell) = a$ for all $k in mathbb{N}$, so in particular $s(f(m))(ell) = a$ for all $ell geq j$, but this contradicts the fact that $s(f(m))$ is a finite string.

Therefore $g(i)$ is undefined for all but finitely many $i$. Let $j$ be the largest such that for all $i leq j$, $g(i)$ is defined. Find $m$ such that $s(f(m+k))(i)$ is constant for all $i leq j$ and is always undefined for $i = j+1$. Since $s(f(m+k))(j+1)$ is always undefined, we have that $s(f(m+k))(ell)$ is always undefined for any $ell > j$, which implies that $k mapsto f(m+k)$ is in fact a constant map, so we have that $f$ is eventually constant, as required. $square$

Now from this lemma we immediately get that if $f : mathbb{N} rightarrow T$ is non-increasing under $sqsubset$, then it is eventually constant, because each $T_n$ is an initial segment of $T$ and $f(0) in T_n$ for some $n$. (Of course this is just the fact that $varepsilon_0$ is well-ordered expressed with a particular notation for elements of $varepsilon_0$, but I won't tell Kronecker if you don't.)

At this point the rest of the proof should be fairly familiar. Given any Goodstein sequence, $g_n$, we associate a sequence of elements of $T$ by converting the hereditary base-$(n+2)$ notation representation of $g_n$ to a finite rooted tree by the following: $0$ corresponds to the tree with a single node and the number $a_k (n+2)^k + a_{k-1} (n+2)^{k-1} + dots + a_0$ corresponds to a tree where for each $ell leq k$, we attach $a_ell$ copies of the tree associated to $ell$ to the root node. It is clear that replacing $n+2$ by $n+3$ does not change the associated tree, but subtracting $1$ does produce a strictly smaller tree under $sqsubset$. If we had a Goodstein sequence which did not terminate it would give us a function $f: mathbb{N} rightarrow T$ which was non-increasing but also not eventually constant, which contradicts our lemma. Therefore every Goodstein sequence must terminate.

---

Regarding the metamathematical properties of this proof, the place where we are using second order arithmetic is in the main induction in the lemma, because the statement is for all functions $f: mathbb{N} rightarrow T_n$, which is using a second-order quantifier. The thing is that we don't really need this full strength for Goodstein's theorem. It is good enough to know it for computable $f$ (since the function associated to a Goodstein sequence is computable), but note that in the inductive proof we use the induction hypothesis on $g(i)$, which is not a priori a computable function, even when $f$ itself is. Furthermore, even though $g(i)$ is in general only a partial function with finite domain (and hence a computable object), this is non-uniform. If we have a family of functions $f_p: mathbb{N} rightarrow T_n$ and we want to know the associated family $g_p(i)$, this will typically require the Turing jump of the family $f_p$ to compute. This is a sign that these proofs won't work very uniformly in Peano arithmetic, especially since unpacking a proof of the lemma for a specific $n$ will end up needing something like $n$ Turing jumps.

We can formalize an encoding of finite rooted trees as natural numbers in Peano arithmetic and prove many basic properties (e.g. everything before the lemma). For any finite $n$ and any family $f_p(k)$ of uniformly definable functions $f_p : mathbb{N} rightarrow T_n$, Peano arithmetic proves the following:

For any parameter $p$, if $f_p : mathbb{N} rightarrow T_n$ is non-increasing, then it is eventually constant.

The whole issue is that $mathsf{PA}$ cannot prove this uniformly in $n$ for sufficiently complicated families $f_p$, such as, for instance, the family of computable functions.