Gödel's incompleteness theorem can't be proven?

I have a very simple question, that I still haven't found an answer to yet: Gödel is said to have proven that Peano Arithmetic (or any system capable of expressing it) can't prove its own consistency.

His proof relies on the notion that we can construct a statement, that, on a meta-level, means "This statement can not be proven" and from this he follows that the arithmetical statement itself cannot be proven.

But if I see it correctly, this conclusion can't be derived formally. As I see it, his proof shows that the statement that is represented ("This statement can't proven") cannot be proven, but not that the statement it is represented with (an arithmetical statement) can't be proven.

Gödels proof confuses meaning with meta-meaning; he follows from the impossibility of proving the meta-statement the impossibility of proving the actual statement, which is not a provably valid step (though it may be intuitively valid, that is debateable).

So, as most mathematicians would disagree with this, how does Gödel show that the statement that the self-referential unprovability statement is represented with can't be proven?

It seems to me Gödel's theorem can't be proven. That a system can't prove its own consistency is just true because it is simply obvious that no system can prove its own consistency for the very simple reason that the notion of consistency ultimately can't be formalized.

Almost all mathematicians would disagree with me, but what is wrong with my argument that Gödel confuses statement and meta-statement (which might be valid, but can't be proven to be valid)?

-
I don't have much time to write an actual answer. Have you considered the case that you are confusing meaning with meta-meaning? Of course it is not a solid argument but almost 90 years have passed and the proofs given were thoroughly studied. If there was a mistake, it would have been founded already. –  Asaf Karagila Jan 12 '12 at 19:08
@AsafKaragila well if Benny misunderstands Godel's incompleteness theorem then that's an even better reason to post the question here, isn't it? –  smackcrane Jan 12 '12 at 19:10
Consistency has a very simply definition, actually! –  Mariano Suárez-Alvarez Jan 12 '12 at 19:11
@smackcrane: Of course, but claiming that he did it wrong, and everyone else disagrees is a very different phrasing than "Where am I wrong?" –  Asaf Karagila Jan 12 '12 at 19:27
Consistency, at least as used in this context, is fully defined meaning essentially "free of contradiction" where contradiction is used in its formal sense of "There exists a p such that both p can be proven to be true and p can be proven to be false." –  TimothyAWiseman Jan 12 '12 at 20:44
show 27 more comments

Let me phrase the argument in somewhat more modern terms:

Goedel constructs a means of encoding any computer program's source code by an arithmetic formula, such that he can prove that, for any program which eventually outputs "YES", Peano Arithmetic (PA) proves the corresponding formula, and for any program which eventually outputs "NO", PA disproves the corresponding formula.

Then Goedel* constructs a computer program with the code "Search through all the possible proofs in PA till you find either a proof or a disproof of the formula corresponding to my source code. If you find a proof first, output 'NO'; if you find a disproof first, output 'YES'. (If you never find either, just keep on searching forever...)" [This is a recursively defined program, in that it refers to its own source code, but that's ok: we understand well how to write up such recursive programs, and even how to compile them to languages that do not directly support recursion. This compilation is essentially what "diagonalization" does]

Now, let p be the formula corresponding to this program's source code. So long as PA either proves or disproves p, this program will eventually output something. But if this program outputs 'YES', then PA must prove p (by the second paragraph) and also disprove p (this is the only way the program ever outputs 'YES'). Similarly, if this program outputs 'NO', then PA must disprove p (by the second paragraph) and also prove p (this is the only way the program ever outputs 'NO'). Thus, if PA either proves p OR disproves p, it necessarily proves p AND disproves p; they're a package deal. So if PA is "complete", then it is inconsistent.

That is the mechanism of the result. It's quite concrete and doesn't depend on any handwavy arguments about meta-statements. It's just a matter of A) knowing how to construct computer programs which can access their own source code, and B) having an appropriate representation of such programs in PA (or whatever system one is interested in), in the sense of the properties of the second paragraph of this post.

[*: I say Goedel, but I actually mean Rosser, five years later; I've chosen to use his approach (which yields a slightly stronger result than Goedel in this context, albeit one which generalizes less) because I think it might be simpler to discuss for now]

-
Slight correction. If PA both proves and disproves p, the output is either YES or NO, depending on which proof is found first. Either output would imply that PA both proves and disproves p. The point remains that if PA proves p it must also disprove p, and vice versa. –  Robert Israel Jan 12 '12 at 19:54
Whoops, sorry; I meant to account for that! Thanks for catching that; I've fixed it now. –  Sridhar Ramesh Jan 12 '12 at 20:01
Your restatement helps illustrate the relationship between the incompleteness therom and the halting problem. The construction is essentially identical. A key difference is that the halting problem proves it's program p does not exist at all, while the program p for the incompleteness theorm does exist. You should note more explicitly that the program will run forever if PA cannot prove or disporve p, (thus making it incomplete). You imply that, but never state it outright. –  Kevin Cathcart Jan 12 '12 at 22:06
In computational terms, Goedel's result is the undecidability of the halting problem, as you note, while Rosser's result is the uncomputability of every total function extending the partial function which sends programs to their outputs. –  Sridhar Ramesh Jan 14 '12 at 6:30