Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
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

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]

share|cite|improve this answer
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
This formulation is on shaky ground. At the risk of sounding like a crackpot, the halting problem may yet fall. – Joshua Feb 26 '15 at 23:29

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.

share|cite|improve this answer
With meaning and meta-meaning I just mean the statement that is encoded and the statement that this statement is encoded with. I am not objecting to any interpretation, I am just asking where in the proof Gödel showed the unprovability of the statement that the encoded statement is encoded with, as opposed to the unprovability of the statement that is being encoded, since I don't see where he did. – Benny Jan 12 '12 at 21:53
Hi, Jim! About "model", I was wondering what differences are between its formal meaning and its usual informal sense, e.g. a mathematical model of fluid flow or protein folding? Are they inherently related? Thanks! – Tim Jan 13 '12 at 13:30
Did Godel actually write a completely formal proof where everything in his proof got completely formalized in a symbolic language like that of proofs of say quantifier exchange equivalences in formal logic? If not, and as I understand it he didn't (mainly because something like his theorem seems too hard to do that), the emphasis on "has" in "has been proved" I simply don't see as warranted when someone expresses some skepticism here. – Doug Spoonwood Jan 13 '12 at 17:23
@Tim There are a few formal meanings for the word "model" in mathematical logic. See and They're arguably not very related to the informal use of the word model. – Jim Belk Jan 14 '12 at 17:39

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.