incompletenesslogic
Gödel's first incompleteness theorem states that "…For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system".
What does it mean that a statement is true if it's not provable?
What is the difference between true and provable?
We have to hedge quite a bit in what you said. First, there are many complete theories: the theory of all groups of order 7 is complete, as an example. However, Gödel showed that any "nice enough" (read: "recursively enumerable") consistent first-order theory capable of encoding basic arithmetic is incomplete. (There is a complete theory of number theory, usually denoted $\mathrm{Th}(\mathbb{N})$, which consists of all sentences that are true in the standard model of number theory; unfortunately, this is not a "nice enough" theory — it's impossible to program a computer to print out all and only the axioms of this theory!)
Also, these statements that you gave, $\mathsf{(G)CH}$, $\mathsf{AC}$, are not provably unprovable in $\mathsf{ZF}$. However, it is provable that they are unprovable in $\mathsf{ZF}$ only if $\mathsf{ZF}$ is itself inconsistent.
This is what a relative consistency result means: it is a result that says the consistency of one theory implies the consistency of the other. Kurt Gödel proved that if $\mathsf{ZF}$ is consistent, then so if $\mathsf{ZFC}+\mathbf{V}=\mathbf{L}$ (and also that $\mathsf{ZFC}+\mathbf{V}=\mathbf{L}$ implies $\mathsf{GCH}$). Paul Cohen proved that if $\mathsf{ZF}$ is consistent, then both $\mathsf{ZF}+\neg\mathsf{AC}$ and $\mathsf{ZFC}+\neg\mathsf{CH}$ are consistent. More elementarily, with $\mathsf{ZF}$ one can construct the natural numbers, and so the consistency of $\mathsf{ZF}$ implies the consistency of $\mathsf{PA}$. These are fundamentally relative consistency results, and cannot be improved to straight consistency results. This stems from Gödel's Second Incompleteness Theorem. Because of this the acceptance of the consistency of $\mathsf{ZF(C)}$ is an article of faith (though one I'm happy to believe in).
I recommend that you look at the first page of George Boolos's Gödel's second incompleteness theorem explained in words of one syllable (Mind, vol.103, pp.1-3). It is a quite entertaining look at the meaning of Gödel's Second Incompleteness Theorem.
Before discussing any of the technical issues associated with your question: Yes, in order to ensure that a statement (about numbers) is true (in the standard model), we currently do not have any procedure other than exhibiting a proof. (In fact, most mathematicians would argue that this is the only way to meaningfully discuss truth.) If the statement is unprovable in $\mathsf{PA}$, such a proof by necessity is in a stronger system, typically a fragment of set theory, $\mathsf{ZFC}$, sometimes a fragment of second order arithmetic, $\mathsf{Z}_2$. But sometimes we go beyond $\mathsf{ZFC}$. The typical extensions we consider usually assume large cardinals. There is a well justified body of evidence indicating that it makes sense to say that proofs of arithmetic statements in these systems are indeed true (I link to a small discussion on these matters near the end).
(Since proof is at the heart of this discussion, you may be interested is a series of essays by computer scientists, mathematicians, and philosophers, on The nature of mathematical proof that was published in the journal Philos. Trans. R. Soc. Lond. Ser. A Math. Phys. Eng. Sci, vol 363, No. 1835, Oct 15, 2005. Sadly, the only link I have is behind a paywall.)
There is a technical difference between the sentences produced by Gödel's techniques (or Rosser's) and sentences such as the strong Ramsey theorem that the Paris-Harrington theorem discusses. (For additional examples, see here and the references listed there.)
Gödel's statement is $\Pi^0_1$, that is, it has the form $\forall n\,\psi(n)$ where $\psi$ is a recursive statement (in the language of arithmetic, all its quantifiers are bounded). The strong Ramsey theorem is $\Pi^0_2$, that is, it has the form $\forall n\,\exists m\,\psi(n,m)$, where $\psi$ is recursive.
$\Pi^0_1$ are meaningful statements even by strict finitistic standards (see for example Richard Zach's dissertation and his discussion of Tait's analysis of Hilbert's program). They are true if they are unprovable (in fact, $\mathsf{PA}$ proves every sentence $\phi$ that is true of the natural numbers and such that $\lnot\phi$ is $\Pi^0_1$): If $\exists n\,\psi(n)$ is true, then for some number $m$, we can prove this statement simply by verifying $\psi(m)$ which, being a recursive statement, has a straightforward verification -- informally, we run a computer program that is guaranteed to halt, and check that the program outputs $\mathtt{Yes}$.
On the other hand, $\Pi^0_2$ statements cannot be called finitistic. If unprovable, this does not automatically ensure their validity (or falsehood). However, they admit a natural interpretation: They state that certain recursive function is total (if the sentence is $\forall n\,\exists m\,\psi(n,m)$, the function $f(n)=m$ assigns to each $n$ the least $m$ such that $\psi(n,m)$), that is, they state that certain computer program will halt, no matter its input. Typical independent $\Pi^0_2$ statements have the peculiarity that the corresponding recursive function is fast growing (see for example this discussion, or my article on Goodstein sequences). By a theorem of Wainer, there is a standard mathematical approach to verifying their unprovability, namely, one checks that the function $f$ under discussion eventually dominates the first $\varepsilon_0$ functions in a fast growing hierarchy.
One could consider Gödel statements and the like as first generation independence statements, and the more "combinatorial" $\Pi^0_2$ statements that followed as second generation. The mathematical arguments involved in either case are really very different. A third generation family of independence statements would be $\Pi^0_1$ combinatorial statements, so they are finitistic in the sense of Hilbert's program, but they have immediate, apparent mathematical (as opposed to meta-mathematical) meaning. Such a family of statements is considered of great interest. Remarkably, recent work of Harvey Friedman has produced such examples, see for example his book on Boolean relation theory, available at his page.
This is by no means the end of the story. For example, we now have a whole family of independent meta-mathematical statements of increased complexity of which $\mathrm{Con}(\mathsf{PA})$ (the sentence in the second incompleteness theorem) is but the weakest possible. See for example Aspects of Incompleteness by Per Lindström, or Metamathematics of first-order arithmetic by Petr Hájek and Pavel Pudlák. In the context of set theory, we can go further, as the completeness theorem tells us that set theory is consistent if and only if $\mathrm{Con}(\mathsf{ZFC})$ holds. We can go beyond this and require the existence of an $\omega$-model (one whose set of natural numbers is isomorphic to the standard model) or even stronger, the existence of a $\beta$-model (that is, a well-founded model). Woodin has explained how his $\Omega$-logic provides in a sense an ultimate extension to this process.
We also have families of $\Pi^0_2$ statements whose truth is harder and harder to verify. For example, the Paris-Harrington theorem gives a result that is not only independent of $\mathsf{PA}$ but also independent of the theory obtained by adding to $\mathsf{PA}$ all true $\Pi^0_1$ statements. But it is easy to verify once we go beyond this theory. On the other hand, Friedman identified a finite form of Kruskal's tree theorem that cannot be verified by so-called predicative means, which means that adding it to $\mathsf{PA}$ gives us a system with consistency strength significantly higher than that of $\mathsf{PA}$ with, say, Goodstein's theorem.
And we can go beyond, as Friedman has examples of $\Pi^0_2$ statements whose proof requires assumptions of a large cardinal character (typically, the existence of Mahlo cardinals of all finite orders, but recent examples go much further).
In set theory we study the consistency strength hierarchy, and have identified remarkable structure, starting with the identification of the large cardinal hierarchy. For a brief and somewhat technical discussion of these issues, see here. The point is that we can see these results as extending significantly beyond arithmetic the realm of what is true but unprovable (in specific formal systems).
Best Answer
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.