Is Goodstein's theorem equivalent to $\varepsilon_0$-induction over weak base theories (e.g. PRA)?

Question

Is Goodstein's theorem equivalent to $\varepsilon_0$-induction over a weak base theory like PRA? I'm surprised this hasn't been asked here before (as far as I can tell).

Answer 1

Rathjen proved that the Goodstein theorem proves $\mathsf{PRWO}$, which states that there is no decreasing primitive recursive sequence of ordinals $<\epsilon_0$, over $\mathsf{PRA}$. You may refer the following article for the proof:

Rathjen, Michael. "Goodstein’s theorem revisited." in Gentzen's Centenary: The Quest for Consistency. Springer, Cham, 2015. 229-242.

On the other hand, we can encode the standard proof of the Goodstein theorem by using $\mathsf{PRWO}$ and Cantor normal form of ordinals $<\epsilon_0$: Every Goodstein sequence yields a computable sequence of decreasing ordinals. In fact, it is primitive recursive - we know how to compute the Goodstein sequence by using bounded loops. Thus if there is a counterexample of Goodstein's theorem, then $\mathsf{PRWO}$ fails.

I do not know $\mathsf{PRWO}$ is equivalent to $\epsilon_0$-induction (at least for primitive recursive relations), though.

---

(Added in 23 April 2021) I found that Arai's textbook stated the following theorem (Theorem 4.1(e) of his textbook):

Theorem. $\mathsf{I\Sigma_1}$ proves $\mathsf{PRWO}$ is equivalent to the 1-consistency of $\mathsf{PA}$.

Arai stated this theorem under different terminology. He uses $\mathscr{E}^\omega DS_{\epsilon_0}$ for $\mathsf{PRWO}$. Also, his original statement is more general than I mentioned. Note, however, that $\mathsf{I\Sigma_1}$ is stronger than $\mathsf{PRA}$.