Goodstein at the Second Threshold: An Independence Result for $ID_2$
Abstract
The classical Goodstein process, defined via hereditary base- 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 . By defining -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 () 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}
}