Article contents
GOODSTEIN SEQUENCES BASED ON A PARAMETRIZED ACKERMANN–PÉTER FUNCTION
Published online by Cambridge University Press: 02 July 2021
Abstract
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,
$\Sigma ^1_1$
-DC
$_0$
, ATR
$_0$
, up to ID
$_1$
. 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.
- Type
- Articles
- Information
- Copyright
- © The Association for Symbolic Logic 2021
References
![](https://static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20210915114240428-0441:S1079898621000305:S1079898621000305_inline733.png?pub-status=live)
![](https://static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20210915114240428-0441:S1079898621000305:S1079898621000305_inline734.png?pub-status=live)
- 2
- Cited by