Heuristic interpretations of the PA-unprovability of Goodstein's Theorem

Question

I've relatively recently learned about Goodstein's Theorem and its unprovability in Peano arithmetic (the Kirby-Paris Theorem). I do not have any real knowledge of formal logic; but I think I've seen it explicitly or implicitly suggested in various places that a heuristic interpretation of the PA-unprovability of Goodstein's Theorem is:

"Even though Goodstein's Theorem is a finite statement about finite numbers, nevertheless -- in contrast to PA-provable statements -- it is necessary to invoke infinity to be able to prove Goodstein Theorem. This is reflected in the fact that infinite ordinals are typically used in the proof of Goodstein's Theorem, although it is possible to prove Goodstein's Theorem without explicitly using theory of infinite ordinals."

My question is: Is the above a fairly common way for the PA-unprovability of Goodstein's Theorem to be described; and if so, to what extent should this heuristic description be considered correct/helpful?

---

More on my thoughts behind asking this question:

After seeing the responses to my question Which part(s) of this proof of Goodstein's Theorem are not expressible in Peano arithmetic? [where I tried to write as painfully explicitly constructive a proof of Goodstein's Theorem as I could, and asked at what points that proof goes out of PA], I started to feel like the above heuristic is misleading. The point at which my proof failed to remain within PA was not where I was expecting.

If I have understood correctly (and this may be a big "if", so please correct me if I've got something wrong):

The usual proof of Goodstein's Theorem is based on the fact that there does not exist a strictly decreasing sequence of ordinals less than $\epsilon_0$; but this fact is not a theorem of PA.

However:

• For any given integer $k \geq 1$, the set of ordinals less than $\omega \uparrow\uparrow k$ is constructible in PA (and one doesn't have to view this metaphysically as a kind of "infinity", but rather it can be viewed as a set of formal expressions [or if you prefer, functions of a natural-number-valued variable called $\omega$] in Cantor normal form, equipped with the lexicographical order).
• If you suppose you have a strictly decreasing sequence $\alpha$ of ordinals less than $\omega \uparrow\uparrow k$ for some specified integer $k \geq 2$, there is a fairly simple procedure to construct from $\alpha$ a strictly decreasing sequence of ordinals less than $\omega \uparrow\uparrow (k-1)$, with the procedure having the following two key properties:

1. The procedure -- along with the proof that the procedure works -- can be written out in a manner that has no dependence on $k$ and $\alpha$ themselves, besides the need to substitute the specified $k$-value and $\alpha$ into a few placeholders (that are not themselves dependent on $k$ and $\alpha$).
2. For each possible $k$-value, this procedure and its proof exists entirely within PA.

Accordingly, for any starting value $p$ for a Goodstein sequence, one of the possible PA-proofs that the resulting Goodstein sequence terminates is:

1. Suppose for a contradiction that it doesn't terminate.
2. Take an integer $k_0 \geq 1$ such that $p < 2\uparrow\uparrow k_0$.
3. Take the sequence of ordinals less than $\omega \uparrow\uparrow k_0$ constructed as in the usual non-PA proof of Goodstein's Theorem, and call it $\alpha_0$.
4. Now do the following:

• If $k_0>1$, write out the above-described procedure and proof with $\alpha_0$ and the value of $k_0$ substituted into the placeholders, to get a strictly decreasing sequence of ordinals less than $\omega \uparrow\uparrow (k_0-1)$, and call that $\alpha_1$.
• Then, if $k_0>2$, write out the above-described procedure and proof with $\alpha_1$ and the value of $k_0-1$ substituted into the placeholders, to get a strictly decreasing sequence of ordinals less than $\omega \uparrow\uparrow (k_0-2)$, and call that $\alpha_2$.
• Then, if $k_0>3$, write out the above-described procedure and proof with $\alpha_2$ and the value of $k_0-2$ substituted into the placeholders, to get a strictly decreasing sequence of ordinals less than $\omega \uparrow\uparrow (k_0-3)$, and call that $\alpha_3$.
• Keep going with this until you've repeated the above process $k_0-1$ times, to give a sequence called $\alpha_{\text{whatever the value of $k_0-1$ is}}$.

5. You've now constructed a strictly decreasing sequence of ordinals less than $\omega$, which is effectively the same as a strictly decreasing sequence of natural numbers, giving a contradiction. QED

Assuming the soundness of PA, the act of spelling out the details of the five above steps essentially constitutes a proof of Goodstein's Theorem; but this proof is not expressible in PA because: even though step 4 can be implemented in PA for any given value of $k_0$, the general command to perform the recursion in step 4 cannot be expressed in PA.

Two concluding thoughts:

1. If it is the case that heuristic discussions of Goodstein's Theorem identify the 'infinity-ness' of PA-unprovability with the fact that 'infinite ordinals' typically appear in the proof, then this seems to me to be conflating two different infinities: The use of infinite ordinals less than an a pre-specified infinite ordinal less than $\epsilon_0$ is (from what I understand) perfectly admissible in PA; the "infinity" in the above-described proof of Goodstein's Theorem responsible for making it not a PA proof is found in the fact that the recursion in the general statement of step 4 is a recursive construction of infinite sequences.

2. In the beautiful question Could Kronecker accept a proof of Goodstein's theorem?, I imagine it is implicitly assumed that Kronecker would be willing to accept the soundness of PA, while obviously being unhappy with Cantor's new set theory. Now if my above discussion of a way to prove Goodstein's Theorem is correct, then it would seem pretty clear that if Kronecker (or whoever else) would have been willing to accept the soundness of PA (which itself seems pretty reasonable) then he wouldn't for a moment have complained about the above proof! So I suspect that the arising of that question is itself evidence that typical heuristic framings of the PA-unprovability of Goodstein's Theorem are misleading.

I repeat my emphasis that everything above in this post is based on my limited understanding, which could be wrong, and part of what I'm asking for in this post is correction on anything I've got wrong.

Answer 1

You've shown how to prove, in PA, the statement "the Goodstein sequence starting with $p$ terminates" for any given $p$. But once $p$ is given, that statement has a proof in PA that just consists of computing the Goodstein sequence one term at a time until it reaches $0$.

Now let me say something about your real question: What does it mean to say that proving a certain theorem requires using infinity? First, there is a natural set of axioms, which I'll call FIN, for reasoning about (hereditarily) finite sets, namely the ZFC axioms with the axiom of infinity replaced by an axiom saying that every set is finite. Just as our ordinary reasoning about arbitrary sets can be formalized on the basis of the ZFC axioms, so our ordinary reasoning about finite sets can be formalized on the basis of FIN. (These are empirical facts about our reasoning, as the word "ordinary" suggests.) So a natural way to say that a theorem requires infinity for its proof is to say that this theorem is not a consequence of the FIN axioms.

Second, I need to say what all this has to do with PA. That's based on one mathematical fact (a theorem, not something empirical), namely that PA is the same as FIN in the following sense. Any statement about (hereditarily) finite sets can be reformulated as a statement about natural numbers (by Gödel numbering), and the original statement is provable in FIN iff the reformulation is provable in PA. And conversely, any statement about natural numbers can be reformulated as a statement about (hereditarily) finite sets (by using finite von Neumann ordinals to represent natural numbers), and the original statement is provable in PA iff the reformulation is provable in FIN.

Personally, I prefer to think in terms of FIN; if someone really wants PA then I'll reformulate as above after I've finished thinking. I suspect the reason many people prefer to state results (like unprovability of Goodstein's theorem) in terms of PA is that it's easier to tell people what the PA axioms are.

The parenthetical "hereditarily" above just means that we deal with finite sets whose elements are also finite, and so are their elements, etc. The point is that we don't allow cheaters to say that they deal only with finite sets but then smuggle infinite sets into the proof as elements of some of their finite sets.

Answer 2

To my way of thinking, the arguments you mention seem not to distinguish sufficiently between the content of Goodstein's theorem as a universal claim $\forall p$ and Goodstein's theorem as a collection of individual statements $\varphi_p$ about particular numbers $p$.

You are arguing in effect that we should take ourselves to have proved Goodstein's theorem if we have a scheme of methods for seeing separately that each $\varphi_p$ is true.

But the theory PA is able to prove every single instance, for any particular $p$, which is after all a (long but) simple calculation — no complicated theory required. What it is not able to do is to prove the universal claim $\forall p$ as a single statement. There is no way to unify your separate individual arguments into a single provable formalism.

The universal claim is stronger than the theory of its specific instances, and we should really think of it that way. One can see how this can be in the case of PA and Goodstein by thinking about the possibility of nonstandard models of PA. In a nonstandard model of PA in which Goodstein's theorem fails, all the standard $p$ still have successful terminating instances, and the violation will occur only with some nonstandard $p$ in that model. But it is with these nonstandard $p$ that the scheme of your argument breaks down. It is in this sense that your reasoning is not really formalizable in PA. You don't actually have a general method that truly applies to all numbers in the PA sense, since if you did, it should work with all the numbers in any PA model, but it doesn't. This is the sense in which you don't have a PA proof.

There are many other occurrences of this kind of local/uniform dichotomy phenomenon. For example, for any particular finite set $S$ of PA axioms, then PA proves that $S$ is consistent. And the consistency of PA itself is the universal assertion, that every finite subset of PA is consistent. And yet, PA cannot prove that, in light of the second incompleteness theorem.

Another instance is that for any finite list of formulas in the language of set theory, ZFC proves that there is some ordinal $\theta$ such that those formulas are absolute between $V_\theta$ and the full universe $V$. In particular, for every finite subtheory of ZFC, the theory ZFC proves that it is true in some $V_\theta$. But ZFC does not prove the universal claim that every finite subtheory of ZFC is true in some $V_\theta$.

Similarly, if you consider the decision problem to determine whether program $p$ halts strictly before $q$ (on trivial input, say), then this is undecidable, since with it by using a $q$ that never halts, we could solve the halting problem. But for any fixed $p$ we can decide it for $q$, since either $p$ never halts, in which case it doesn't halt before $q$, or $p$ halts in some fixed number of steps, and we can check $q$ for that long to decide it.

So in general, there is a difference between having a unified single solution for the general case and having separate individual solutions for each individual case.

For the same reason, to prove Goodstein's theorem it doesn't suffice to convince us by a scheme of separate arguments that each instance is true. We cannot actually prove the universal claim from the set of those particular instances.