I am interested to know, possibly in non-technical lay terms, which axioms are really needed to prove the Goodstein's theorem: http://en.wikipedia.org/wiki/Goodstein's_theorem and/or other theorems of that type. It is claimed that it cannot be proved in first order arithmetic. My first question is: What exactly is missing in first order arithmetic which is needed to prove the theorem? Is it perhaps the induction axiom? The theorem has been proved by using trans-finite numbers. But that's very strange, given that the theorem talks only about finite numbers. My second question is: Can the theorem be proved without using trans-finite numbers?