< Back to previous page

Publication

Goodstein sequences on a parametrized Ackermann-Peter function

Journal Contribution - Journal Article

Following our [6], though with somewhat different methods here, further variants of Goodstein sequences are introduced in terms of parameterized AckermannU+2013Pé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, U+03A311 -DC 0 , ATR 0 , up to ID 1 . The key is the so-called U+201CHardy hierarchyU+201D of proof-theoretic bounding finctions, providing a uniform method for associating Goodstein-type sequences with parameterized normal form representations of positive integers.
Journal: BULLETIN OF SYMBOLIC LOGIC
ISSN: 1943-5894
Issue: 2
Volume: 27
Pages: 168 - 186
Publication year:2021
Accessibility:Closed