Fast Goodstein Walks
David Fern\'andez-Duque, Andreas Weiermann

TL;DR
This paper introduces a variant of the Goodstein process using fast-growing functions, proving its termination and maximal length, with implications for the limits of certain formal theories.
Contribution
It defines a new Goodstein process based on fast-growing functions and proves its termination and maximal length, extending understanding of ordinal analysis.
Findings
The process terminates despite unprovability in certain theories.
It achieves maximal length among similar processes.
Implications for the limits of formal proof systems.
Abstract
We define a variant of the Goodstein process based on fast-growing functions and show that it terminates, but this fact is not provable in Kripke-Platek set theory or other theories of strength the Bachmann-Howard ordinal. We moreover show that this Goodstein process is of maximal length, so that any alternative Goodstein process based on the same fast-growing functions will also terminate.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
