(Im)possibility to prove the Goodstein's theorem

[Demystifier]

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?

 

[jedishrfu]

In the wiki article on Peano axioms they say that adding the multiply operation allows them to drop the second order axiom

http://en.wikipedia.org/wiki/Peano_axioms

The Peano axioms contain three types of statements. The first axiom asserts the existence of at least one member of the set "number". The next four are general statements about equality; in modern treatments these are often not taken as part of the Peano axioms, but rather as axioms of the "underlying logic".[3] The next three axioms are first-order statements about natural numbers expressing the fundamental properties of the successor operation. The ninth, final axiom is a second order statement of the principle of mathematical induction over the natural numbers. A weaker first-order system called Peano arithmetic is obtained by explicitly adding the addition and multiplication operation symbols and replacing the second-order induction axiom with a first-order axiom schema.

 

[Demystifier]

Thanks for the remark, but I don't see how is this related to the (im)possibility to prove the Goodstein theorem.

 

[jedishrfu]

Thanks for the remark, but I don't see how is this related to the (im)possibility to prove the Goodstein theorem.

I was answering your simpler question regarding the induction principle.

Perhaps others here can comment on your larger question.

 

[Demystifier]

I have just found the answer to my question:
http://mathoverflow.net/questions/134590/goodsteins-theorem-without-transfinite-induction

So more-or-less as I expected, "Goodstein's theorem does not necessarily require transfinite induction for its proof, but it's not provable in elementary arithmetic. It can be proved by ordinary induction on a statement involving quantification over sets."

Which leads me to the next question:
Is there a known natural (non-self-referential) statement in second-order arithmetic which can neither be proved nor disproved in second-order arithmetic?