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

Question

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)?

Answer 1

This strikes me as a strangely philosophical objection to a mathematical theorem. Whether or not you agree with the standard interpretation of Gödel's Theorem has no relevance to the question of whether Gödel's Theorem has been proven. Gödel's Theorem has been proven -- all of the terms used in the statement of the theorem have been defined rigorously, and the conclusion follows from the premises in a rigorous way. Concerns about meaning and meta-meaning have no relevance to the proof, because "meaning" and "meta-meaning" are not rigorously defined terms, and nothing in the proof references these ideas.

It is reasonable to object to the standard interpretation of Gödel's Theorem. In some sense, Gödel constructed a mathematical model of mathematics itself, and proved that certain statements about mathematics are true in his model. (Note: I'm using the word "model" here in the usual informal sense, e.g. a mathematical model of fluid flow or protein folding.) There is no doubt that Gödel's model in fact has these properties, but you may or may not agree that mathematics actually has these properties, depending on whether you think the model is accurate.

Answer 2

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]