Goodstein's theorem is a famous example of an arithmetical statement that is unprovable in $\mathsf{PA}$ but provable in a stronger theory. It is well-known that Goodstein's theorem implies the consistency of $\mathsf{PA}$, but I have barely seen a precise characterization for its strength.
Rathjen mentioned two versions of Goodstein sequences in his Goodstein revisited, one is the general one and the other is the special Goodstein sequence, which is the sequence used in Wikipedia version of Goodstein's theorem. A general Goodstein sequence is similar to a special Goodstein sequence but it allows changing the base under a given monotone function (so when we compute the $(n+1)$-th term, we change base $f(n)$ to $f(n+1)$.) The special Goodstein sequence is a Goodstein sequence with $f(n)=n+2$.
Rathjen also stated that
Theorem. The following are equivalent over $\mathsf{RCA_0}$:
- Every Goodstein sequence terminates.
- There is no infinite descending sequence over $\varepsilon_0$.
It is well-known that the latter is equivalent to the uniform $\Pi^1_1$-reflection scheme for $\mathsf{ACA}_0$, so it raises the following question: Rathjen also stated in the same paper that
Theorem. The following are equivalent over $\mathsf{PA}$:
- Every special Goodstein sequence terminates. (Equivalently, every primitive recursive Goodstein sequence terminates.)
- There is no primitive recursive infinite descending sequence over $\varepsilon_0$.
Based on the complexity of the statement of these two, let me ask the following:
Question. Are the following two equivalent over $\mathsf{PA}$?
- There is no infinite descending primitive recursive sequence over $\varepsilon_0$.
- Uniform $\Pi^0_2$-reflection for $\mathsf{PA}$: If a $\Pi^0_2$-sentence $\sigma$ is provable in $\mathsf{PA}$, then $\sigma$ is true.
If my question fails, is there any known characterization for 1 in terms of uniform reflection or something similar?
