Goodstein Sequences Based on a Parametrized Ackermann–péter Function

Following our [6], though with somewhat different methods here, further variants of Goodstein sequences are introduced in terms of parameterized Ackermann–Péter functions. Each of the sequences is shown to terminate, and the proof-theoretic strengths of these facts are calibrated by means of ordinal assignments, yielding independence results for a range of theories: PRA, PA, Σ ¹₁ -DC ₀ , ATR ₀ , up to ID ₁ . The key is the so-called “Hardy hierarchy” of proof-theoretic bounding finctions, providing a uniform method for associating Goodstein-type sequences with parameterized normal form representations of positive integers.