I would say that the Von Neumann construction and PA try to capture the natural numbers. It is a philosophical stance which can be called platonism. What you say is called the formalist stance.
What I mean is that since Goodstein's theorem is provably true for the naturals, but is not a consequence of the Peano axioms, then the definition of the naturals used to demonstrate Goodstein's must be strictly stronger than the Peano axioms themselves. I was wondering what this definition might be.
I'm familiar with the distinction between formalism and Platonism, although I still haven't made my mind up yet :)
It is a consequence of the Peano arithmetic (Peano axioms plus definition of addition and multiplication), it is just not provable in this system.
Gödel's first incompleteness theorem [1] states this fact, that no theory above a certain expressiveness (read as can express natural numbers with addition and multiplication) can be consistent and complete. Assuming Peano arithmetic is consistent, it can not be complete and complete means you can prove all true facts expressible in the system within the system itself.
The (standard) proof of Goodstein's theorem uses ordinal numbers [2] which are outside of Peano arithmetic and the Kirby–Paris theorem proves that there is no proof inside Peano arithmetic [3].
