11
$\begingroup$

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

$\endgroup$
0

2 Answers 2

Reset to default
28
$\begingroup$

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]

$\endgroup$
5
  • 1
    $\begingroup$ 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. $\endgroup$
    – Robert Israel
    Jan 12, 2012 at 19:54
  • $\begingroup$ Whoops, sorry; I meant to account for that! Thanks for catching that; I've fixed it now. $\endgroup$
    – Sridhar Ramesh
    Jan 12, 2012 at 20:01
  • 6
    $\begingroup$ 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. $\endgroup$
    – Kevin Cathcart
    Jan 12, 2012 at 22:06
  • $\begingroup$ 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. $\endgroup$
    – Sridhar Ramesh
    Jan 14, 2012 at 6:30
  • $\begingroup$ In the spirit of using modern terms for the post, you might prefer to say"this is a reflectively defined program" instead of recursive. $\endgroup$
    – DanielV
    Nov 8, 2017 at 15:21
19
$\begingroup$

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.

$\endgroup$
6
  • 3
    $\begingroup$ 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. $\endgroup$
    – Benny
    Jan 12, 2012 at 21:53
  • 1
    $\begingroup$ 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! $\endgroup$
    – Tim
    Jan 13, 2012 at 13:30
  • 1
    $\begingroup$ 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. $\endgroup$
    – Doug Spoonwood
    Jan 13, 2012 at 17:23
  • 1
    $\begingroup$ @Tim There are a few formal meanings for the word "model" in mathematical logic. See en.wikipedia.org/wiki/Interpretation_(logic) and en.wikipedia.org/wiki/Structure_(mathematical_logic). They're arguably not very related to the informal use of the word model. $\endgroup$
    – Jim Belk
    Jan 14, 2012 at 17:39
  • $\begingroup$ Severely disagree with this. You could replace "Gödel's Theorem" with "the existence of Russel's paradoxical set" and all the same characterizations would apply. It's existence was proven. It was proven in terms of things even more rigorously defined that the framework for GIT. But to suggest that when encountering an unsound seeming result in logic, that there are always going to be demonstrably true but not provably true claims, then you should turn your brain off and accept it as "proven" ? That is exactly the time to start considering design decisions and "meta-meaning". $\endgroup$
    – DanielV
    Nov 8, 2017 at 15:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .