Godel and Goodstein theorems

I have started reading Penrose's book the Emperor's new mind and came across these interesting theorems in the preface about Godel's and Goodstein's theorem. Here I briefly mention the two following the treatment from the book:

Godel's theorem:

Suppose that we are given a computational procedure P for establishing mathematical assertions of a particularly well defined type such as the Fermat's last theorem. Then if we are prepared to accept the successful derivation of some assertion by use of rules of P provides us with an unassailable demonstration of the truth of that assertion- then we must also accept as unassailably true some other assertion G(P) which is beyond the scope of the rules of P.

Goodstein's theorem:

Consider any positive number, let us say 3. First, we express this as a sum of distinct powers of 2:

3 = 2^1 + 1.

We now apply a succession of simple operations to this expression, these alternating between:

1. increasing the 'base' by 1.
2. subtract 1.

It may seem that the numbers would be ever increasing, but the theorem tells us that no matter what positive number we start with, we always end up with zero!

The reader is encouraged to verify this by taking some number. An example starting with 3 can be seen here: click

What is rather more extraordinary is that Goodstein's theroem is actually a Godel theorem for the procedure of mathematical induction. Recall that mathematical induction provides a way of proving that some mathematical statement S(n) holds for all n = 1,2,3 ... The procedure is to show that if it holds for n =1, then it also holds for n+1. If P stands for the procedure of mathematical induction, then we take G(P) to be Goodstein's theorem.