Goodstein sequences and unprovability in Peano arithmetic

Abstract

Goodstein’s theorem is a true finitary statement about the natural numbers which is nevertheless unprovable in the theory of Peano Arithmetic. Throughout this thesis, we prove this claim, following closely the methods of Buchholz and Wainer [1987]. This process leads us through various important results in the study of proof theory. We begin by establishing the ordinal numbers and ordinal arithmetic, from which we prove Goodstein’s theorem. In this process, we introduce the ordinal ε0, around which many of our results center. Moreover, we establish a hierarchy of fast growing functions up to ε0, following Ketonen and Solovay [1981]. Using these functions, we determine a formula for Goodstein’s function following Caicedo [2007], and prove bounding results for elementary functions. Moreover, we establish the machinery required to define PA, namely first order logic and a Tait-style proof system. In defining PA, we embed in our language the Csillag-Kalmar elementary functions, which allows for a neat definition of the provably computable functions of PA. As was done in Gentzen [1964] to prove the consistency of Peano Arithmetic, we embed PA in an infinitary system PA∞. This allows us to perform cut-elimination, essentially reducing the variation of how a proof is derived at the cost of a longer proof. This allows us to obtain a bound for the provably computable functions, which we can show does not hold for Goodstein’s function by the formula derived previously. This can be used to show that Goodstein’s theorem is unprovable in PA.