$\begingroup$
PA is enough, because PA can encode computation.
This is longer than I expected, and was made longer still by some browser crashes. But I'd been idly thinking of writing these ideas up. I hadn't for these reasons.
It is a lot of work. What I have to say is obvious to logicians, and they would consider the detour into programming to only be a distraction. Computer programmers who can appreciate the programming detour, are mostly not that interested in logic.
But this question hits the perfect intersection, and so I'll outline my thoughts in some detail. First I will answer the question in detail, assuming that anything you can do by a mechanical process (for example on a computer), can be done in PA. Then I will explain how PA encodes computation by outlining how to bootstrap Lisp from PA. If you're curious about bootstrapping Lisp, search for "Prelude". Otherwise, read on.
To answer this question, it suffices for PA to be able to prove how long the proof must be for any particular $G(n)$, and to prove that it can construct that proof. I will show this by demonstrating that PA can construct a proof of length $O(\log^*(n) \log(\log^*(n)))$, where the funny function is the very slowly growing iterated logarithm. In general, it takes more work to write out $n$, than it does to write out a partial proof of Goodstein's theorem which covers $n$!
But since larger values of $n$ need longer proofs, this doesn't lead to a proof in PA of Goodstein's theorem.
First a detour into the roots of Goodstein's theorem.
What are ordinals?
In John Von Neumann's famous construction, you get ordinals in ZFC from the following rules.
... continue reading