Goodstein theorem without transfinite numbers?

[Demystifier]

It is known that the Goodstein theorem
http://en.wikipedia.org/wiki/Goodstein's_theorem
which is a theorem about natural numbers, cannot be proved from the standard axioms of natural numbers, that is Peano axioms http://en.wikipedia.org/wiki/Peano_axioms .

It is also known that Goodstein theorem can be proved from a more powerful axiom system which includes transfinite numbers.

My question is: Can Goodstein theorem be proved from a natural axiom system more powerful than Peano axioms, but without transfinite numbers?

I expect that it can. More precisely, I suspect that Peano axioms cannot prove the Goodstein theorem because these axioms do not contain an axiomatization of powers (but only of addition and multiplication). If one would add appropriate natural axioms for powers (similar to those for addition and multiplication), I expect that then one could prove the Goodstein theorem without transfinite numbers.

Can someone confirm or reject my expectations?

 

[Citan Uzuki]

I'm not sure. Certainly the theory PA + "all Goodstein sequences terminate" proves Goodstein's theorem without mentioning transfinite numbers, but it's probably not what you would consider a "natural" axiom system. I can state with certainty that adding axioms for exponents would not enable you to prove anything not already provable in PA, because exponentiation can be defined in terms of addition and multiplication, and its basic properties are provable theorems. Indeed, were this not the case, it would be impossible to even state Goodstein's theorem in the language of PA.

 

[Demystifier]

Thanks for a convincing answer. I thought that exponentiation might not be definable in PA in terms of multiplication in the same sense in which, in Presburger arithmetic, multiplication is not definable in terms of addition. But as you said, Goodstein theorem can be stated in PA, which means that exponentiation must be definable.