Hostname: page-component-74656f9884-j7cmm Total loading time: 0 Render date: 2026-11-07T09:11:02.385Z Has data issue: false hasContentIssue false

GOODSTEIN SEQUENCES BASED ON A PARAMETRIZED ACKERMANN–PÉTER FUNCTION

Published online by Cambridge University Press:  02 July 2021

TOSHIYASU ARAI
Affiliation:
UNIVERSITY OF TOKYO TOKYO, JAPAN E-mail: tosarai@ms.u-tokyo.ac.jp
STANLEY S. WAINER
Affiliation:
UNIVERSITY OF LEEDS LEEDS, UK E-mail: s.s.wainer@leeds.ac.uk
ANDREAS WEIERMANN
Affiliation:
UNIVERSITY OF GHENT GHENT, BELGIUM E-mail: andreas.weiermann@ugent.be
Rights & Permissions [Opens in a new window]

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.

Information

Type
Articles
Copyright
© The Association for Symbolic Logic 2021