True vs. Provable

Consider this claim: John Smith will never be able to prove this statement is true.

If the statement is false, then John Smith will be able to prove it's true. But clearly that can't be, since it's impossible to prove that a false statement is true. (Assuming John Smith is sensible.)

If it's true, there's no contradiction. It just means John Smith won't be able to prove it's true. So it's true, and John Smith won't be able to prove it's true. This is a limit on what John Smith can do. (So if John Smith is sensible, there are truths he cannot prove.)

What Goedel showed is that for any sensible formal axiom system, there will be formal versions of "this axiom system cannot prove this claim is true". It will be a statement expressible in that formal system but, obviously, not provable within that axiom system.

Provable means that there is a formal proof using the axioms that you want to use. The set of axioms (in this case axioms for arithmetic, i.e., natural numbers) is the "system" that your quote mentions. True statements are those that hold for the natural numbers (in this particular situation).

The point of the incompleteness theorems is that for every reasonable system of axioms for the natural numbers there will always be true statements that are unprovable. You can of course cheat and say that your axioms are simply all true statements about the natural numbers, but this is not a reasonable system since there is no algorithm that decides whether or not a given statement is one of your axioms or not.

As a side note, your quote is essentially the first incompleteness theorem, in the form in which it easily follows from the second.

In general (not speaking about natural numbers only) given a structure, i.e., a set together with relations on the set, constants in the set, and operations on the set, there is a natural way to define when a (first order) sentence using the corresponding symbols for your relations, constants, and operations holds in the structure. ($\forall x\exists y(x\cdot y=e)$ is a sentence using symbols corresponding to constants and operations that you find in a group, and the sentence says that every element has an inverse.)

So this defines what is true in a structure. In order to prove a statement (sentence), you need a set of axioms (like the axioms of group theory) and a notion of formal proof from these axioms. I won't eleborate here, but the important connection between true statements and provable statements is the completeness theorem:

A sentence is provable from a set of axioms iff every structure that satisfies the axioms also satisfies the sentence.

This theorem tells you what the deal with the incompleteness theorems is: We consider true statements about the natural numbers, but a statement is provable from a set of axioms only if it holds for all structures satisying the axioms. And there will be structures that are not isomorphic to the natural numbers.

Note that you are not paraphrasing the 2nd Incompleteness Theorem (which says that an axiomatic system that satisfies certain technical conditions cannot prove its own consistency unless it is inconsistent), but rather the First Incompleteness Theorem.

Remember that a "model" of an axiomatic system means a particular interpretation of the primitive notions that makes that makes the axioms true in that interpretation.

"True" and "False" in this context refer to models. "True" should really be "true in the model $M$"; that is, there is a particular interpretation of the axioms which makes the statement true. When we talk about arithmetic statements being "true", we mean "true in the standard model" (the "standard model" being a particular interpretation of the primitive notions of arithmetic). See for example Wikipedia's page on non-standard models of airthmetic.

"Provable" means that there is a formal derivation of the statement from the axioms. If a statement is provable, then it is true in all models; conversely, Gödel's Completeness Theorem shows that if a (first order) statement is true in all models, then it is provable.

In particular, a statement is "formally undecidable" in an axiomatic system if there are some models in which it is true, and some models in which it is false. When you have a "prefered model" (as we do with arithmetic), we often talk simply about "true" instead of "true in a particular model".