I was asked in email about a good source about Goodstein sequences and the independence of Goodstein’s Theorem from Peano Arithmetic. The independence result is due to Kirby and Paris in a 1983 paper in the Proceedings of the London Mathematical Society (vol. 14), using the method of indicators. Georg Moser suggested the following paper by Cichon, which appeals to the characterization of provably recursive functions in PA only:
E. A. Cichon, A Short Proof of Two Recently Discovered Independence Results Using Recursion Theoretic Methods. Proceedings of the American Mathematical Society 87/4 (1983), 704-706. JSTOR
Cichon’s proof can also be found in Fairtlough and Wainer’s chapter on “Hierarchies of Provably Recursive Functions” in the Handbook of Proof Theory, S. Buss, ed. (Elsevier, 1998).