Goodstein sequences for the Bachmann-Howard ordinal

David Fernández-Duque, Ghent University. Part of the Proofs, Constructions and Computations Seminar Series.

The classical Goodstein process is defined by writing numbers in base k for increasing values of k and successively subtracting one.  By mapping the numbers obtained into epsilon_0, it becomes clear that the process must terminate in finite time, although the sequences are typically too long for this termination to be observed empirically.

In this talk we will consider an alternate Goodstein-like process based on subrecursive hierarchies.  Namely, one uses a form of fast-growing hierarchy based on ordinals below epsilon_0 to provide a notation system for natural numbers relative to some base number k.  With this one can produce an analogue to the classical Goodstein process which can also be guaranteed to terminate, although in this setting one must map natural numbers into the Bachmann-Howard ordinal, producing a proof of termination not formalizable in ID_1.