# Predicatively unprovable termination of the Ackermannian Goodstein process

## TL;DR

This paper investigates a variant of the Goodstein process based on the Ackermann function, demonstrating that while these sequences eventually terminate, their termination cannot be proven within predicative frameworks.

## Contribution

It introduces an Ackermannian Goodstein process and proves its termination is unprovable in predicative systems, extending understanding of provability limits.

## Key findings

- Ackermannian Goodstein sequences terminate
- Termination is unprovable in predicative systems
- Extends classical Goodstein results to Ackermannian case

## 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.