Goodstein sequences for prominent ordinals up to the Bachmann-Howard ordinal (Q408160)

Goodstein sequences give a well-known and easy-to-state principle that is independent of Peano arithmetic. The idea is to code the ordinals below \(\varepsilon_0\) by natural numbers and to mimic a slow stepping-down function on the ordinals by a simple combination of elementary operations on the natural numbers (change of base and predecessor). In this paper the authors generalize the idea of Goodstein sequences to higher ordinals and corresponding systems of arithmetic, up through the Howard-Bachmann ordinal \(\varphi_{\epsilon_{\Omega+1}}\) and the system \(\mathrm{ID}_1\). The key idea is to define the generating rule of the sequences directly on the structure of the terms representing the ordinals in some canonical ordinal notation system. In particular one has to define the analog of the ``\(-1\)'' stepping-down operation in this general setting. The method allows to define Goodstein sequences corresponding to ordinals up through the Howard-Bachmann ordinal. The theorems asserting that the sequences terminate are unprovable in the corresponding systems of arithmetic, up through \(\mathrm{ID}_1\). For example, Goodstein sequences with no termination proof in Peano arithmetic plus transfinite induction up to \(\Gamma_0\) are obtained along the way. The proposed method avoids the problems of uniqueness of representation arising if one insists in coding the ordinal terms by integers. As a tradeoff, this choice makes the ``number-theoretic'' nature of the resulting statements less immediate compared to the original Goodstein sequences for \(\varepsilon_0\).