Goodstein sequences for prominent ordinals up to the Bachmann-Howard ordinal. (English) Zbl 1251.03069
Goodstein sequences give a well-known and easy-to-state principle that is independent of Peano arithmetic. The idea is to code the ordinals below \(\varepsilon_0\) by natural numbers and to mimic a slow stepping-down function on the ordinals by a simple combination of elementary operations on the natural numbers (change of base and predecessor).
In this paper the authors generalize the idea of Goodstein sequences to higher ordinals and corresponding systems of arithmetic, up through the Howard-Bachmann ordinal \(\varphi_{\epsilon_{\Omega+1}}\) and the system \(\mathrm{ID}_1\).
The key idea is to define the generating rule of the sequences directly on the structure of the terms representing the ordinals in some canonical ordinal notation system. In particular one has to define the analog of the “\(-1\)” stepping-down operation in this general setting. The method allows to define Goodstein sequences corresponding to ordinals up through the Howard-Bachmann ordinal. The theorems asserting that the sequences terminate are unprovable in the corresponding systems of arithmetic, up through \(\mathrm{ID}_1\). For example, Goodstein sequences with no termination proof in Peano arithmetic plus transfinite induction up to \(\Gamma_0\) are obtained along the way.
The proposed method avoids the problems of uniqueness of representation arising if one insists in coding the ordinal terms by integers. As a tradeoff, this choice makes the “number-theoretic” nature of the resulting statements less immediate compared to the original Goodstein sequences for \(\varepsilon_0\).
In this paper the authors generalize the idea of Goodstein sequences to higher ordinals and corresponding systems of arithmetic, up through the Howard-Bachmann ordinal \(\varphi_{\epsilon_{\Omega+1}}\) and the system \(\mathrm{ID}_1\).
The key idea is to define the generating rule of the sequences directly on the structure of the terms representing the ordinals in some canonical ordinal notation system. In particular one has to define the analog of the “\(-1\)” stepping-down operation in this general setting. The method allows to define Goodstein sequences corresponding to ordinals up through the Howard-Bachmann ordinal. The theorems asserting that the sequences terminate are unprovable in the corresponding systems of arithmetic, up through \(\mathrm{ID}_1\). For example, Goodstein sequences with no termination proof in Peano arithmetic plus transfinite induction up to \(\Gamma_0\) are obtained along the way.
The proposed method avoids the problems of uniqueness of representation arising if one insists in coding the ordinal terms by integers. As a tradeoff, this choice makes the “number-theoretic” nature of the resulting statements less immediate compared to the original Goodstein sequences for \(\varepsilon_0\).
Reviewer: Lorenzo Carlucci (Rome)
MSC:
| 03F15 | Recursive ordinals and ordinal notations |
| 03D20 | Recursive functions and relations, subrecursive hierarchies |
| 03F30 | First-order arithmetic and fragments |
References:
| [1] | Abrusci, V. Michele, Some uses of dilators in combinatorial problems. III. Independence results by means of decreasing \(F\)-sequences \((F\) weakly finite dilator), Arch. Math. Logic, 29, 2, 85-109 (1989) · Zbl 0701.03028 |
| [2] | Cichon, E. A., A short proof of two recently discovered independence results using recursion theoretic methods, Proc. Amer. Math. Soc., 87, 4, 704-706 (1983) · Zbl 0512.03028 |
| [3] | Cichon, E. A.; Wainer, S. S., The slow-growing and the Grzegorczyk hierarchies, J. Symbolic Logic, 48, 2, 399-408 (1983) · Zbl 0567.03020 |
| [4] | Friedman, Harvey; Sheard, Michael, Elementary descent recursion and proof theory, Ann. Pure Appl. Logic, 71, 1, 1-45 (1995) · Zbl 0821.03027 |
| [5] | Goodstein, R. L., On the restricted ordinal theorem, J. Symbolic Logic, 9, 33-41 (1944) · Zbl 0060.02306 |
| [6] | Goodstein, R. L., Transfinite ordinals in recursive number theory, J. Symbolic Logic, 12, 123-129 (1947) · Zbl 0030.00401 |
| [7] | Kirby, Laurie; Paris, Jeff, Accessible independence results for Peano arithmetic, Bull. Lond. Math. Soc., 14, 4, 285-293 (1982) · Zbl 0501.03017 |
| [8] | Frederik Meskens, Andreas Weiermann, Classifying phase transition thresholds for accessible independence results. Preprint 2008.; Frederik Meskens, Andreas Weiermann, Classifying phase transition thresholds for accessible independence results. Preprint 2008. · Zbl 1378.03040 |
| [9] | Weiermann, Andreas, Some interesting connections between the slow growing hierarchy and the Ackermann function, J. Symbolic Logic, 66, 2, 609-628 (2001) · Zbl 0993.03074 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
