Knuth's intuition that Goldbach might be unprovable Knuth's intuition that Goldbach's conjecture (every even number greater than 2 can be written as a sum of two primes) might be one of the statements that can neither be proved nor disproved really puzzles me.  (See page 321 of http://www.ams.org/notices/200203/fea-knuth.pdf )
All the examples of such statements I have heard until now were very abstract, but this one is so concrete.
My question is that is there such an example of a statement of this sort that is proved to be unprovable,  i.e., for some property $P(n)$, the statement that "every natural number $n$ satisfies $P(n)$".  (In the Goldbach case $P(n)$ would be "if $n$ is an even number greater than $2$, then there exists two primes $p$ and $q$ such that $n = p + q$".)
If Knuth is right, it would be very interesting in one sense: the negation of Goldbach is obviously provable if it is true.  So if someone proves that Goldbach is not provable, then we would know that Goldbach is true.  We would be sure that someone would never come up with an example that would violate the condition.  For the practical person, this is as good as it is proven.
Edit: I have learned a lot from the answers, thank you so much!
 A: In the paper "Skolem and pessimism about proof in mathematics" 
(Phil. Trans. R. Soc. A 2005 363, p.2409) Paul  Cohen wrote:
"The view that I shall present differs somewhat from this, and is in a sense more
radical, namely that it is unreasonable to expect that any reasoning of the type
we call rigorous mathematics can hope to resolve all but the tiniest fraction of
possible mathematical questions."
A: It's equivalent to asking about possibilities such as "aliens land on Earth and provide us a proof that Peano Arithmetic can't prove Goldbach", or "an ancient cuneiform tablet is found containing an RSA-encrypted proof that Riemann Hypothesis is independent of Zermelo-Fraenkel set theory".   Although in such a scenario Goldbach (resp. RH) would be found to be PA-unprovable, that would happen only as a result of developments so stupendous that Goldbach and its provability become trifling afterthoughts, and one might as well ask directly about probability of alien landings or Babylonian codices.
The only currently known way for Goldbach to be unprovable is if within the additive combinatorics of the prime numbers were encoded a model of Peano Arithmetic (ie., PA could derive a model of itself from a PA-constructible function $g$ such that for all $n>1$, $g(n)$ and $(2n - g(n))$ are odd primes).   This would imply a degree of rigidity and intricate structure in the primes so far beyond the existing ideas --- such as the expectation that weak analogues of geometry and topology are manifested in algebraic number theory (zeta functions), or that some degree of probabilistic (quasirandom) structure exists in additive number theory --- as to completely dwarf any mathematics that currently exists.   
The equally earth-shaking alternative means by which Goldbach could be shown to transcend PA, is if entirely new methods are found for demonstrating PA-unprovability of relatively "generic" (ordinary, concrete) mathematical statements.  Presumably this would mean that not only Goldbach, but a very large number of other open conjectures would be seen to also transcend Peano Arithmetic (and, in the process, be solved in a stronger system such as ZF).  A general machine for turning a large volume of conjectures into ZFC theorems with PA unprovability certificates would, in the same way as the alien landings, be of such overwhelming importance and surprise as to make Goldbach itself irrelevant.
While any future discoveries are hypothetically possible, the only existing evidence for the demonstrable PA-unprovability of Goldbach (i.e., for the idea that a proof will be found in a stronger theory, such as ZF, that Goldbach transcends PA) is the body of Goedel-type unprovability and independence results derived in the past 80 years, and nothing in that or any other branch of mathematics suggests either the prospect of incredibly fine structure in the primes or of generic methods for showing unprovability.   So to talk seriously of Goldbach or the Riemann Hypothesis being shown to be PA-unprovable is essentially an unadulterated speculation that a totally new species of mathematics will be discovered, a speculation that is not related to any specific feature of any particular number theoretic problem.
A: You are right to view the Goldbach conjecture as having a particularly simple logical form. Such statements of the form "for every $n$, property $P(n)$ holds", where $P$ is a particularly simple statement, are known in logic as the $\Pi_1$ statements. These are one step up from the bottom at the entryway to the arithmetic hierarchy. Nevertheless, several of the most famous independence results concern statements at this level of complexity.

*

*For example, consistency statements have this complexity. The assertion Con(PA) that the first order Peano Axioms are consistent has the same complexity as Goldbach's conjecture, since it can be viewed as the statement "for every finite sequence of symbols, it is not the proof of a contradiction in PA". But the Incompleteness Theorem shows that if PA is consistent, then Con(PA) is independent of PA, so it is an instance of your phenomenon.


*Similarly, Con(ZFC) and other consistency statements are independent and have complexity $\Pi_1$, the same as the Goldbach conjecture.


*Similarly, the famous "I am not provable" statement $\sigma$ of Goedel has complexity $\Pi_1$, for it can be viewed as asserting "for every finite sequence of symbols, it is not a proof of $\sigma$". This statement is true but unprovable (in PA, say), because if it were provable, then it would be false; and so it is not provable, and hence true.


*Another example arising in considering the halting problem. It is not difficult to prove that there is a particular Turing machine program $p$ such that $p$ does not halt, but this fact is unprovable. (Otherwise, we would be able to solve the halting problem, by searching either for halting behavior or proofs of non-halting.) The statement "for every number $n$, program $p$ does not halt in $n$ steps" is therefore therefore true but unprovable, and has the same $\Pi_1$ complexity as the Goldbach Conjecture.


*In contrast, the Goodstein theorem, which is provable in ZFC but independent of PA, has a higher complexity than Goldbach, since it is the statement "for every $n$, there is a stage $k$ at which the Goodstein sequence for $n$ reaches $0$". Thus, it has complexity $\Pi_2$, with two alternations of quantifiers.


*Also, the Paris-Harrington example also has complexity $\Pi_2$, since they have the form "for every $n$, $m$ and $k$, there is a number $N$ such that every $k$-coloring of the $m$-subsets of $N$, there is a good monochromatic subset of size $n$".
Finally, let me remark that before Fermat's Last Theorem was proved, it was often remarked that perhaps FLT might be independent, and logicians dreamed longingly about this possibility. FLT also has complexity $\Pi_1$, since it asserts "for all nonzero $a$, $b$, $c$ and $n\gt 2$, then $a^n+b^n\neq c^n$." But meanwhile, Wiles has proved it, and so our hopes are dashed. (One interesting point is that Wiles' proof is certainly not in PA, but in ZFC or technically, ZFC + Universes, so it is conceivable still that it could be independent of PA.) But perhaps we should class Knuth's remarks about Goldbach along with these previous remarks about FLT---the longings of logicians for a big splash!
A: Again from combinatorics: The strengthened finite Ramsey theorem>. It was proved by Paris and Harrington that it is true, but not provable in Peano arithmetic. Wikipedia says: "This was the first "natural" example of a true statement about the integers that could be stated in the language of arithmetic, but not proved in Peano arithmetic".
A: The simplest example I can think of is Goodstein's theorem. This, as the name suggest, is provable (in the standard ZFC theory of sets) but is not provable in Peano arithmetics.
I don't want to duplicate Wikipedia, but briefly here is how it goes. Take a number, say $47$ and write it in base $2$, so you get $$47 = 1 \cdot 2^5 + 1 \cdot 2^3 + 1 \cdot 2^2 + 1 \cdot 2^1 + 1 \cdot 2^0.$$ Write each exponent in base $2$, rinse and repeat until you cannot simplify anymore. In our case you get
$$47 = 1 \cdot 2^{1 \cdot 2^{1\cdot 2^{1 \cdot 2^0}} + 1 \cdot 2^0} + 1 \cdot 2^{1 \cdot 2^{1 \cdot 2^0} + 1 \cdot 2^0} + 1 \cdot 2^{2^{1 \cdot 2^0}} + 1 \cdot 2^{1 \cdot 2^0} + 1 \cdot 2^0.$$
After that subtitute each $2$ with a $3$ and subtract $1$, to get
$$1 \cdot 3^{1 \cdot 3^{1\cdot 3^{1 \cdot 3^0}} + 1 \cdot 3^0} + 1 \cdot 3^{1 \cdot 3^{1 \cdot 3^0} + 1 \cdot 3^0} + 1 \cdot 3^{3^{1 \cdot 3^0}} + 1 \cdot 3^{1 \cdot 3^0} + 1 \cdot 3^0 - 1 = 3^{28} + 81 + 27 + 3.$$
Write this number again in expanded base $3$ (in our case we already have it), change each $3$ with a $4$ and subtract $1$ (this time the expanded form will change a bit since we do not have a final $1$).
Proceed in this way and you get a sequence (called the Goodstein sequence of $n$) which becomes abnormously big at a really fast rate and... well, this sequence is eventually $0$. Just subtracting that small $1$ at each step eventually becomes preponderant over the base substitution.
The fact that the Goodstein sequence of $n$ is eventually $0$ is really easy to prove using ordinals, but it turns out it is an unprovable statement with only Peano arithmetics.
A: Others have mentioned several theorems (Goodstein, Paris-Harrington, Robertson-Seymour, Kruskal) that are unprovable from the axioms of first-order Peano arithmetic.  However, these theorems are provable in ZFC, and in fact from much weaker axioms than ZFC.  In particular, they are all accepted by the mathematical community as "proven" (unlike, for example, the continuum hypothesis).  Although Knuth did not say explicitly what set of axioms he was thinking of, my guess is that he was thinking of axioms with roughly the same logical strength as ZFC.  If your question is whether there are any "natural" mathematical statements with the same finitary flavor as Goldbach's conjecture that have been proved to be unprovable in ZFC (assuming ZFC is consistent), then the answer is no.
There is no intrinsic reason why such a finitary statement cannot be proved to be unprovable in ZFC.  After all, "ZFC is consistent" is a finitary statement and it is unprovable in ZFC (again, assuming ZFC is consistent).  Now, "ZFC is consistent" is not a "natural" mathematical statement like Goldbach's conjecture is; it is a contrived statement obtained by means of diagonalization.  But there is no reason in principle that a natural statement like Goldbach cannot be unprovable in ZFC.  Harvey Friedman has devoted a significant portion of his career to finding examples of natural finitary mathematical statements that are provably unprovable in ZFC.  One of his best examples to date appears towards the end of Martin Davis's Notices article on The Incompleteness Theorem.  In my opinion this is a very concrete statement in graph theory that one could imagine coming up as a technical lemma in a graph theory paper.
However, I must admit that I do not find Knuth's reasoning particularly convincing.  In my opinion, Knuth makes the common mistake of conflating the psychological difficulty of coming up with a proof with the logical strength needed to prove a theorem.  There are many mathematical theorems with difficult proofs whose proofs can nevertheless be formalized in very weak logical systems.  Conversely, there are theorems like Paris-Harrington that have easy proofs but whose proofs require more than the usual logical strength.  So just because we have no idea how to prove something does not, in my view, provide any compelling evidence that it is independent of some strong logical system like ZFC.
A: A $\Pi_1^0$ statement is one of the form $\forall n\,\varphi(n)$, where $\varphi(n)$ is some recursively verifiable statement about $n$. This can be made more precise, but I want to keep the description this way, to give an idea of what some of the issues are. The negation of $\Pi^0_1$ statement, if true, is easily provable: After all, all it says is that some fixed number $n_0$ must have an easily verifiable property. You just have to exhibit a counterexample explicitly and it is straightforward to verify its validity.
In practice, of course, we know that there are computational issues that this ignores, but the point remains. 
However, it is not so clear that, if true, a $\Pi^0_1$ statement must be provable. And, in fact, that is not the case. Goedel showed this, but his examples are not particularly natural. Now, if you prove that a $\Pi^0_1$ statement is not decidable from PA, the standard (first order) axioms of number theory, then of course the result must be true. Otherwise, its negation would have been provable.  
There are a few natural combinatorial $\Pi^0_1$ statements that cannot be verified in PA. Harvey Friedman has worked hard to produce examples of this kind with intrinsic combinatorial interest (if not yet immediate appeal to number theorists), because most natural examples are more complicated: $\Pi^0_2$, essentially assertions that some function is total: For all $n$ there is some $m$ for which something straightforward to verify holds. 
Ferretti mentioned Goodstein's theorem, and auniket mentioned Paris-Harrington. I like Goodstein's theorem, because a few years ago I managed to find a formula for the function that computes how long it takes the sequence starting with $n$ to stop. Since this is not provable in PA, the formula was just beyond what can be grasped in first order number theory, and that, I found very interesting. 
A variant of Paris-Harrington is a result of Kanamori-McAloon, with which I've also done some work, showing combinatorially that the version for pairs gives rise to a function that grows precisle as Ackermann's function. The point is: Just because something is beyond the grasp of a formal system, does not mean it is beyond our comprehension. Very interesting combinatorics can still happen here.
Stillwell mentioned the graph minor theorem. This is more interesting, in that not only they are beyond PA, but also beyond significant strengthenings of PA.
All of these examples are provable in ZFC, the basic system of axioms of set theory. Harvey Friedman has produced natural examples that go beyond ZFC and involve large cardinals. His page is full of nice examples of this kind, mostly $\Pi^0_2$, but also (recently) several interesting $\Pi^0_1$ ones. 
Still, as pointed out by agcl, in all of the $\Pi^0_1$ examples, there is a natural sense in which, once we show the statement is independent of the formal system, then we actually have that it is true.
Although Goldbach's conjecture is $\Pi^0_1$, another very famous problem in number theory, the twin primes conjecture, is not, at least not with our current knowledge. Neither it nor its negation are obviously true if verified independent. I am not saying there is any evidence whatsoever for assuming the twin primes conjecture is independent of PA, in fact, that would be more than unexpected. However, it is much more natural to expect that a natural $\Pi^0_2$ statement, such as this one, is independent, than it is to expect that for a $\Pi^0_1$. And it would be very interesting, because then we would need a different method for verifying its truth, since we would have consistency of both the statement and its negation, and no clear evidence of which holds in the usual (standard) model ${\mathbb N}$. 
Coda: A recent thread mentioned a paper where it is claimed that all current approaches, if they show the independence of a $\Pi^0_2$ statement from PA, actually also show it from the (much) stronger system obtained by adding to PA all the true $\Pi^0_1$ statements. Although the claim is something of an exaggeration, it can be made more precise in terms of what kind of model theoretic arguments are used to show the independence. The natural combinatorial examples listed above all fall in this category: They are true, they are independent of PA, and they remain independent in the theory resulting from strengthening PA as explained. Harvey Friedman's examples in ZFC are more interesting in this regard.
[Edited to fix some obvious unintentional lies.]
A: When we say that a statement is undecidable, this is implicitly with regard to some axiom system, such as Peano arithmetic or ZFC.  The reason why statements about arithmetic can be undecidable is that there exist inequivalent models of arithmetic that obey such axiom systems (this is a consequence of the Godel completeness and incompleteness theorems, assuming of course that the axiom system being used is consistent and recursively enumerable).  For instance, the standard or "true" natural numbers obey the Peano axioms, but so do some more exotic number systems (e.g. the nonstandard natural numbers).  It is conceivable that a given statement in arithmetic, such as Goldbach's conjecture, holds for the true natural numbers but not for some other number systems that obey the Peano axioms, though personally I view this possibility as remote.  (Note that the nonstandard natural numbers satisfy exactly the same first-order statements as the standard natural numbers, by Los's theorem, but one can also construct other, weirder, models of arithmetic which have a genuinely different theory.)
So, if Goldbach's conjecture is undecidable for some given axiom system, what this would imply is that every "true" even natural number larger than 4 is the sum of two primes (otherwise we could disprove Goldbach with an argument of finite length), but that there exists a more exotic number system (larger than the true natural numbers) obeying those axioms which contains some even exotic number that is not the sum of two (exotic) primes.  (Note that the length of a proof has to be true natural number, rather than an exotic one, so the existence of an exotic counterexample cannot be directly converted to a disproof of Goldbach.) This is an unlikely scenario, but not an a priori impossible one (as one can see from the example of Goodstein's theorem or the Paris-Harrington theorem).
[Edit: here, as usual, when talking about things like the "true" natural numbers, one has to work in some external reasoning system which may be distinct from the reasoning system one is analysing the decidability of.  For instance, one may be using ZFC as one's external reasoning system to analyse what can and cannot be decided in Peano arithmetic, with the true natural numbers then being constructed by, say, the von Neumann ordinal construction combined with the axiom of infinity.  Or one could be using an informal external reasoning system, based perhaps on some Platonic beliefs about mathematical objects, that is not explicitly axiomatised.  It's best to keep the external system conceptually distinct from any internal ones being studied, as one can get hopelessly confused otherwise.]
A: There are also some concrete examples in graph theory, such as Kruskal's tree
theorem and the Robertson-Seymour graph minor theorem. These theorems
about infinite sequences of graphs were actually proved (by infinitary methods in combinatorics) before it was realized that they are not provable by finitary methods.
Harvey Friedman devised finite versions of the Kruskal and
Robertson-Seymour theorems that can be stated, but not proved, in Peano arithmetic. In fact, they are "more unprovable" than Goodstein's theorem.
A: I once heard Don Zagier talk of a more general intuition that the quality that may make some natural statements unprovable is the quality of telling you just what you would expect to happen anyway. For example, the statement that pi has infinitely many zeros in its decimal expansion may be hard, or even impossible, to prove precisely because it would be a miracle if it were false -- so that if it is true it doesn't have to have a reason for being true.
Goldbach's conjecture is an interesting case for this heuristic. If one combines appropriate "the primes are random" heuristics with the experimental knowledge that it is true up to some very large finite number, then one can argue that the probability that it is false is absolutely tiny. So it might seem like a prime candidate for Zagier's class of difficult problem. And indeed it is at the very least extremely difficult. But there are closely related theorems, such as Vinogradov's three-primes theorem (that every sufficiently large odd number is the sum of three primes) that are proved by exploiting the random-like behaviour of the primes. That is, in a sense one actually proves the heuristic that tells you that the theorem is what you would expect to be true. From this point of view, what makes Goldbach hard is that the method of proof breaks down badly: the notions of quasirandomness we have just aren't strong enough to guarantee that sumsets of quasirandom sets have no gaps. (They can tell us things like that almost every even number is a sum of two primes, in a pretty strong sense of "almost every".)
So one might say that, given that the techniques break down, Zagier's criterion applies again. But I'm uneasy about this -- number theorists who have thought much harder about Goldbach's conjecture than I have are agreed that the problem is currently out of reach, but I have sometimes heard them speculating in some detail about what a proof might look like. And Vinogradov's three-primes theorem might look like a great candidate for the criterion to someone who didn't know about the circle method.
But I think one can at least say that it is conceivable that Goldbach's conjecture "just happens to be true", whereas a conjecture that asserts something "unlikely" tends, if it is true, to have to be true for a reason.
A: There is already a lot of excellent answers, but I think it is useful to make rigorous your argument that "... if someone proves that Goldbach is not provable, then we would know that Goldbach is true."
You are making the jump from "Goldbach is not provable" to "there exists no counterexample to Goldbach's conjecture". But for that you first needs to assume the consistency of ZFC, because otherwise you can prove anything, and more crucially the soundness of ZFC, i.e., that it only proves true statements, because otherwise "Goldbach is not provable" can be simply a lie.
But if you do assume that ZFC is consistent and sound, then every unprovable statement of the form "for every $n$, property $P(n)$ holds" (for some sufficiently simple $P(n)$) is actually true, as consistency and soundness together with unprovability imply that there exists no counterexample.
This argument I took from the paper "Undecidable problems: a sampler"
arXiv:1204.0299.
EDIT: Corrected, see comments.
A: [Edit: In regards to some so called "open question" above, if the twin prime conjecture is independent from PA then it is false. This is very easy to see, just forget about the formulas: any non-standard model of PA is basically the initial segment N followed by some junk. Now if one can show that Goldbach holds for some non-standard model, it must also hold for the standard model N for obvious reason, since it is a "for all...". Similarly, if the twin prime conjecture is true, then it remains so for any non-standard model, since it suffices to establish the validity by exhibiting infinitely many twin primes in the standard model.]
[Edit: If this is still not clear, what the twin prime conjecture says is essentially that "there are infinitely many" twin primes, so if it's true there are infinitely many "standard numbers" (or numerals if you like) that are twin primes. Now for specific n, checking whether n and n+2 are primes only amounts to bounded quantification (definable by a Delta_0 formula if you are such a big fan of fancy terminology...), which is never going to jump outside omega, therefore all the standard (or genuine) twin primes survive in any non-standard model, and in particular, sticking anything to the end of the standard model is not going to invalidate the fact that there are already infinitely many twin primes below omega.]
Well, the seem to be some misunderstanding...


*

*By "unprovable" it's understood that one meant "unprovable from some formal theory" such as Peano Arithmetic or ZFC, it does not mean that Goldbach's conjecture (provided it's true) cannot have a "mathematical proof", what Knuth said (I think it might not even have a proof) in his bloody paper was utter nonsense! For example the fact that CH is independent from ZFC does not mean that it can't be proved or disproved.

*DELETED

*The existence of a non-standard model that is elementarily equivalent (have the same first order theory) to the standard model is irrelevant, since Goldbach's conjecture could be easily written as a first order sentence.
A: You stated:
"If someone proves that Goldbach is not provable, then we would know that Goldbach is true."
If any proof that Goldbach Conjecture (GC) is unprovable is also a proof of GC -- a contradiction -- such a proof cannot exist,
If GC is false, it is possible to disprove it by providing a counterexample. A counterexample is a type of constructive proof.
Merely proving the existence of a counterexample is a type of non-constructive proof.
It may be the case that GC does not have a non-constructive proof. It may also be possible to prove that GC does not have a non-constructive proof. However such a proof would not rule out the existence of a counterexample, nor would it imply that GC is true.
Knuth's argument is: "X is very unlikely, therefore X is impossible". He goes on to recognize that no proof that "X is impossible" will ever be found.
I think most people's intuition that Goldbach's Conjecture (GC) is true is based on the same flawed probabilistic reasoning. If you play the lottery an infinite amount of times eventually you will win, no matter how astronomical the odds.
So unless there is a reason why a counterexample cannot exist, sooner or later one will occur by pure chance. In other words, if GC is true it ought to be provable; and if GC is false it is disprovable by counterexample.
