English

Goodstein at the Second Threshold: An Independence Result for $ID_2$

Logic 2026-04-02 v1

Abstract

The classical Goodstein process, defined via hereditary base-kk exponential normal form, is a well-known example of a principle unprovable in Peano Arithmetic. In this paper, we generalize this framework by constructing a new Goodstein process based on the Hardy hierarchy. We develop an ordinal notation system utilizing a two-step collapsing procedure, which yields a proof-theoretic ordinal of ψ0ψ1(εΩ2+1)\psi_0\psi_1(\varepsilon_{\Omega_2+1}). By defining kk-normal forms for natural numbers within this system, we introduce a Goodstein-type process and demonstrate that the theory of non-iterated positive inductive definitions for two operators (ID2ID_2) cannot prove its termination. This result establishes a new independence result at the second proof-theoretic threshold, further extending the reach of Goodstein-type principles beyond the Bachmann-Howard level.

Keywords

Cite

@article{arxiv.2604.00771,
  title  = {Goodstein at the Second Threshold: An Independence Result for $ID_2$},
  author = {Oriola Gjetaj and Andreas Weiermann},
  journal= {arXiv preprint arXiv:2604.00771},
  year   = {2026}
}
R2 v1 2026-07-01T11:48:03.840Z