Predicatively unprovable termination of the Ackermannian Goodstein process
Toshiyasu Arai, David Fernández–Duque, Stanley S. Wainer, Andreas Weiermann · Proceedings of the American Mathematical Society · 2019
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.