Goodstein revisited

TL;DR

This paper revisits Goodstein's 1944 work, exploring its historical context and demonstrating that the termination of certain Goodstein sequences is unprovable in PA, using elementary methods accessible in the 1940s or 1950s.

Contribution

It provides an elementary proof of unprovability of Goodstein sequence termination in PA, and discusses historical implications for early independence results in mathematical logic.

Findings

Elementary proof of unprovability of special Goodstein sequences in PA.

Historical analysis suggesting earlier possible proofs of independence results.

Discussion on the significance of Goodstein and Gentzen in incompleteness theorems.

Abstract

Inspired by Gentzen's 1936 consistency proof, Goodstein found a close fit between descending sequences of ordinals epsilon_0 and sequences of integers, now known as Goodstein sequences. This article revisits Goodstein's 1944 paper. In light of new historical details found in a correspondence between Bernays and Goodstein, we address the question of how close Goodstein came to proving an independence result for PA. We also present an elementary proof of the fact that already the termination of all special Goodstein sequences, i.e. those induced by the shift function, is not provable in PA. This was first proved by Kirby and Paris in 1982, using techniques from the model theory of arithmetic. The proof presented here arguably only uses tools that would have been available in the 1940's or 1950's. Thus we ponder the question whether striking independence results could have been proved much earlier? In the same vein we also wonder whether the search for strictly mathematical examples of an incompleteness in PA really attained its "holy grail" status before the late 1970's. Almost no direct moral is ever given; rather, the paper strives to lay out evidence for the reader to consider and have the reader form their own conclusions. However, in relation to independence results, we think that both Goodstein and Gentzen are deserving of more credit.