How can Goodstein's theorem be expressed in PA

Question

I understand Goodstein's Theorem and its proof. I'm trying to understand the proof of why Goodstein's Theorem cannot be proved in PA. However, it's not immediately clear to me that Goodstein's Theorem can even be stated in PA. Obviously I'm not looking for a statement of the theorem in PA, but just some rigorous reasoning that would make it unquestionable that it is possible.

Answer 1

The essential point here is that recursive definitions can be formalized in PA as explicit definitions. Specifically, if we have a recursion of the form $f(0)=a$ and $f(n+1)=g(f(n))$, and if we already know how to formalize $g$ in PA, then we can formalize $f$ by defining $f(n)=z$ to mean "there is an $s$ that codes (via your favorite sequence coding) a finite sequence of length $n+1$, in which the first term is $a$, each subsequent term is obtained by applying $g$ to its predecessor, and the last term is $z$."

In the Goodstein case, $g$ should be the function "increase the base by 1 and then subtract 1," which you can formalize in PA once you know how to handle iterated exponentials and sums. These, in turn, are handled by more applications of the recursion idea above.

A technical point is that, in order to obtain exponentiation, by applying the method above to a recursive definition of exponentiation in terms of multiplication, you need to use a sequence coding scheme that doesn't require exponentiation as a prerequisite. Gödel developed such a scheme; it's also presented in Chapter 6 of Shoenfield's book "Mathematical Logic."