Difference between provability and truth of Goodstein's theorem I have been thinking about the difference between provability and truth and think this example can illustrate what I have been wondering about:
We know that Goodstein's theorem (G) is unprovable in Peano arithmetic (PA), yet true in certain extended formal systems. However, it seems like the theorem has a kind of truth that transcends the formal system you use: if you compute the Goodstein sequence for any natural number, it will end at 0 no matter what formal system you use. If you were to consider the system PA $+$ $\lnot G$, wouldn't G still hold in the sense that you could never find a counterexample? Is any of this true, or am I just misunderstanding something?
 A: Good question!

If you were to consider the system PA + $\neg$G, wouldn't G still hold in the sense that you could never find a counterexample?

This gets at an important subtlety here - the issue of models. Any first-order theory like PA, PA+$\neg$G, ZFC, ... has (assuming it's consistent!) many models. Some theories, like PA, have an "intended model," but by the compactness theorem every (interesting) theory will have lots of nonisomorphic models. In particular, in addition to the standard model $(\mathbb{N}; +, \times, 0,1, <)$ of PA, there will also be lots of "nonstandard" models of PA. These models are difficult to describe (for good reason), but very vaguely they're ordered semirings (like $\mathbb{N}$) with "$\mathbb{N}$-ish" properties - in particular, they have a definable notion of exponentiation which behaves the way we're used to and lets the model talk about "finite" sequences of "numbers." The key difference is that a nonstandard model of PA will have elements which are actually infinite. 
Such a nonstandard element can constitute an apparent failure of G within that model. If $M$ is a model of PA+$\neg$G, then there is some $m\in M$ which according to $M$ is a counterexample to $G$. However, this $m$ won't actually be a "true" natural number: it won't be $0$, or $1$, or $1+1$, or ...

At this point it might help to get a little more concrete. As I said above, nonstandard models of PA are difficult to visualize. However, if we look at a weaker theory of arithmetic - say, Robinson's Q - things get much better. Q is a very weak theory indeed, and has many easily-describable nonstandard models. Perhaps the nicest of these is what I'll call $\mathcal{P}$, the set of integer-coefficient polynomials in one variable $x$ with positive leading coefficient (okay fine and also the zero polynomial should be included). 
$\mathcal{P}$ has a number of bizarre arithmetic properties. For instance, "every number is even or odd" is false in $\mathcal{P}$! The polynomial "$x$" is neither even nor odd, since no element $p$ of $\mathcal{P}$ satisfies either $p+p=x$ or $p+p+1=x$. There are many other examples of such strangeness. (Incidentally, this shows that you need induction to prove that every number is either even or odd! :P)
So what's going on? Well, of course in "reality" (that is, $\mathbb{N}$) every number is even or odd. The problem is that $\mathcal{P}$, while satisfying the axioms of $Q$, has "too many numbers" including some very strange ones which as far as $\mathcal{P}$ is concerned are in fact counterexamples to the statement "every number is either even or odd." So this shows that the statement "every number is either even or odd" can't be proved from $Q$ alone. 
Exactly the same thing is going on with Goodstein's theorem G; it's just that the theory in question being PA, the "bad" models are much harder to visualize and so the independence is more mysterious.
A: It's important not to conflate the system PA with the natural numbers themselves. There are other "nonstandard" models of PA: sets other than the natural numbers that admit definitions of $\{S,+,×\}$ which satisfy all the axioms of PA. (In particular, the Löwenheim–Skolem theorem implies that you can even find uncountable sets that admit such definitions.)
Any nonstandard model of PA would have to contain an isomorphic copy of the "actual" natural numbers, and that copy of the natural numbers would have to satisfy Goodstein's Theorem for the reason you stated, but the "nonstandard" elements of the model might have nonconvergent Goodstein sequences.
