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

TL;DR

This paper introduces a generalized Goodstein process based on the Hardy hierarchy, proving that the theory of non-iterated positive inductive definitions for two operators ($ID_2$) cannot prove its termination, establishing a new independence result.

Contribution

It extends Goodstein principles to the Hardy hierarchy and demonstrates their unprovability in $ID_2$, reaching beyond the Bachmann-Howard level.

Findings

The new Goodstein process terminates unprovably in $ID_2$.

Develops an ordinal notation system with a two-step collapsing procedure.

Establishes a new independence result at the second proof-theoretic threshold.

Abstract

The classical Goodstein process, defined via hereditary base-$k$ 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 $\psi_0\psi_1(\varepsilon_{\Omega_2+1})$. By defining $k$-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 ($ID_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.