Formal Proof of the Weak Goodstein Theorem

For many years, I have been interested in introducing students to the development of complex systems by means of modelling and refinement. To this end, I did not find anything better than presenting many examples of system developments. However, I figured out that my examples were not explicit enough on how (mechanical) proofs are performed. So, besides courses presenting these examples and also some courses in various forms of proofs (propositional calculus, first order predicate calculus, set theory), I decided to study the work of professional mathematicians, thinking that it could be good examples for students. Among the works I already studied and reconstructed are the theorem of Zermelo, the theorem of Cantor-Bernstein, the planar graph theorem of Kuratowski, the topological proof of the infinity of primes of Furstenberg, the intermediate value theorem of Bolzano, the Archimedean property of the set of Real numbers, and others. More recently, I found that the Goodstein theorem was also very interesting. The purpose of this short note is to give some information about this theorem and the way I introduce a weak form of it to students.