Can Goodstein's theorem be expressed as an axiom or axiom scheme in PA?

Question

A statement like $\mathsf{Con(PA)}$ depends (or at least seems to depend) on a specific Gödel numbering. My question is whether Goodstein's theorem may be expressed directly in the language of $\mathsf{PA}$, i.e. without relying on a Gödel numbering (or extending the language by additional predicates or by second order variables). Because the axiom of induction can only be expressed as an axiom scheme in $\mathsf{PA}$, I doubt that Goodstein's theorem can be expressed as a single axiom. But nothing seems to prevent an axiom scheme expressing Goodstein's theorem (especially if we don't care whether it is computable or not). Is there such an axiom scheme, and is this axiom scheme computable?

Answer 1

Goodstein's Theorem just says "for every number $n$" "there is a finite sequence $s$" "such that $s$ has some arithmetically definable property relative to $n$".

So the statement of the theorem can be written as a single arithmetical formula of the form $(\forall n)(\exists s)\Phi(n,s)$ where $\Phi$ is in the language of Peano arithmetic.

The only issue with stating this in PA is how to represent the sequence, but it is straightforward to state the theorem otherwise. Usually, sequences are represented using the method of Godel's $\beta$ lemma, but without any Godel numbering.

There's no need for an axiom scheme, and it is not clear how one would help.

Answer 2

Carl Mummert stated

There's no need for an axiom scheme, and it is not clear how one would help.

in his answer. The "reflected answer" given in the comment at least makes it perfectly clear why it is far from obvious that there's no need for an axiom scheme:

How an axiom scheme might really help here is by generating instances of $(\forall n)(\exists s)\Phi \beta(n,s)$ for all (first-order PA) definable $\beta$-functions $\beta(x_1,x_2,x_3)$ (which can be proved in PA to be $\beta$-functions). This axiom scheme might be a stronger statement than an arbitrary individual instance of this scheme (also I don't know whether it is really stronger).

The replies to that comment got sidetracked by details about whether there is a single $\beta$-function, or whether a $\beta$-function just needs to satisfy the two conditions due to Gödel. But the important point is that there are many different encodings of zero sequences of natural numbers, and Goodstein's Theorem will make a statement about every formula expressing such an encoding. Different formula can express the same encoding, but PA "should be able" to prove that these formulas are equivalent. (In fact, I had some "known theorem" of this sort in mind when I wrote the comments, and mainly decided to write this answer when I noticed that I could no longer recall the details.) However, I can see no "obvious" reason why PA should be able to prove all instances of Goodstein's theorem for different encodings to be equivalent.

---

Carl Mummert stated that no Gödel numbering is required

The only issue with stating this in PA is how to represent the sequence, but it is straightforward to state the theorem otherwise. Usually, sequences are represented using the method of Godel's $\beta$ lemma, but without any Godel numbering.

But "represent the sequence" is similar to a Gödel numbering in that there is no privileged canonical representation of the sequence, even if some representations are simpler than others.