Predicatively unprovable termination of the Ackermannian Goodstein process

Arai, Toshiyasu; Fernández-Duque, David; Wainer, Stanley; Weiermann, Andreas

doi:10.1090/proc/14813

Predicatively unprovable termination of the Ackermannian Goodstein process
HTML articles powered by AMS MathViewer

by Toshiyasu Arai, David Fernández-Duque, Stanley Wainer and Andreas Weiermann PDF

Proc. Amer. Math. Soc. 148 (2020), 3567-3582 Request permission

Abstract:

The classical Goodstein process gives rise to long but finite sequences of natural numbers whose termination is not provable in Peano arithmetic. In this manuscript we consider a variant based on the Ackermann function. We show that Ackermannian Goodstein sequences eventually terminate, but this fact is not provable using predicative means.

References

Wilfried Buchholz and Stan Wainer, Provably computable functions and the fast growing hierarchy, Logic and combinatorics (Arcata, Calif., 1985) Contemp. Math., vol. 65, Amer. Math. Soc., Providence, RI, 1987, pp. 179–198. MR 891248, DOI 10.1090/conm/065/891248
E. A. Cichon, A short proof of two recently discovered independence results using recursion theoretic methods, Proc. Amer. Math. Soc. 87 (1983), no. 4, 704–706. MR 687646, DOI 10.1090/S0002-9939-1983-0687646-0
Wilfried Buchholz, Adam Cichon, and Andreas Weiermann, A uniform approach to fundamental sequences and hierarchies, Math. Logic Quart. 40 (1994), no. 2, 273–286. MR 1271290, DOI 10.1002/malq.19940400212
Matt Fairtlough and Stanley S. Wainer, Hierarchies of provably recursive functions, Handbook of proof theory, Stud. Logic Found. Math., vol. 137, North-Holland, Amsterdam, 1998, pp. 149–207. MR 1640327, DOI 10.1016/S0049-237X(98)80018-9
Solomon Feferman, Systems of predicative analysis, J. Symbolic Logic 29 (1964), 1–30. MR 193006, DOI 10.2307/2269764
Solomon Feferman, Systems of predicative analysis. II. Representations of ordinals, J. Symbolic Logic 33 (1968), 193–220. MR 260589, DOI 10.2307/2269866
Harvey Friedman and Florian Pelupessy, Independence of Ramsey theorem variants using $\varepsilon _0$, Proc. Amer. Math. Soc. 144 (2016), no. 2, 853–860. MR 3430859, DOI 10.1090/proc12759
Gerhard Gentzen, Die Widerspruchsfreiheit der reinen Zahlentheorie, Math. Ann. 112 (1936), no. 1, 493–565 (German). MR 1513060, DOI 10.1007/BF01565428
Kurt Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatsh. Math. Phys. 38 (1931), no. 1, 173–198 (German). MR 1549910, DOI 10.1007/BF01700692
R. L. Goodstein, On the restricted ordinal theorem, J. Symbolic Logic 9 (1944), 33–41. MR 10515, DOI 10.2307/2268019
R. L. Goodstein, Transfinite ordinals in recursive number theory, J. Symbolic Logic 12 (1947), 123–129. MR 22537, DOI 10.2307/2266486
R. L. Graham and B. L. Rothschild, Ramsey’s theorem for $n$-dimensional arrays, Bull. Amer. Math. Soc. 75 (1969), 418–422. MR 237349, DOI 10.1090/S0002-9904-1969-12202-0
Laurie Kirby and Jeff Paris, Accessible independence results for Peano arithmetic, Bull. London Math. Soc. 14 (1982), no. 4, 285–293. MR 663480, DOI 10.1112/blms/14.4.285
Jeff Paris and Leo Harrington, A mathematical incompleteness in Peano arithmetic, Handbook of mathematical logic, Stud. Logic Found. Math., vol. 90, North-Holland, Amsterdam, 1977, pp. 1133–1142. MR 3727432
Wolfram Pohlers, Proof theory, Universitext, Springer-Verlag, Berlin, 2009. The first step into impredicativity. MR 2457679
Stephen G. Simpson, Friedman’s research on subsystems of second-order arithmetic, Harvey Friedman’s research on the foundations of mathematics, Stud. Logic Found. Math., vol. 117, North-Holland, Amsterdam, 1985, pp. 137–159. MR 835257, DOI 10.1016/S0049-237X(09)70158-2
Stephen G. Simpson, Subsystems of second order arithmetic, 2nd ed., Perspectives in Logic, Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, 2009. MR 2517689, DOI 10.1017/CBO9780511581007
Andreas Weiermann, Some interesting connections between the slow growing hierarchy and the Ackermann function, J. Symbolic Logic 66 (2001), no. 2, 609–628. MR 1833466, DOI 10.2307/2695032
Andreas Weiermann, A very slow growing hierarchy for $\Gamma _0$, Logic Colloquium ’99, Lect. Notes Log., vol. 17, Assoc. Symbol. Logic, Urbana, IL, 2004, pp. 182–199. MR 2088773
Andreas Weiermann, Classifying the provably total functions of PA, Bull. Symbolic Logic 12 (2006), no. 2, 177–190. MR 2223920
Andreas Weiermann, Ackermannian Goodstein principles for first order Peano arithmetic, Sets and computations, Lect. Notes Ser. Inst. Math. Sci. Natl. Univ. Singap., vol. 33, World Sci. Publ., Hackensack, NJ, 2018, pp. 157–181. MR 3700862
Andreas Weiermann and Wim Van Hoof, Sharp phase transition thresholds for the Paris Harrington Ramsey numbers for a fixed dimension, Proc. Amer. Math. Soc. 140 (2012), no. 8, 2913–2927. MR 2910777, DOI 10.1090/S0002-9939-2011-11121-3
Hermann Weyl, The continuum, Dover Publications, Inc., New York, 1994. A critical examination of the foundation of analysis; Translated from the German by Stephen Pollard and Thomas Bole; With a foreword by John Archibald Wheeler and an introduction by Pollard; Corrected reprint of the 1987 translation [Thomas Jefferson Univ. Press, Kirksville, MO; MR1040831 (91h:01105)]. MR 1280464