2
$\begingroup$

This is a naive question and I haven't actually read the paper itself (I've read this). But from my understanding he demonstrated that it is possible to encode the statement "This statement cannot be proved" using Gödel numbers...

I've also heard that 'the truth of this statement is obvious to humans' (paraprashing Roger Penrose).

But it occurred to me that I thought proof by contradiction was a valid form of proof right? So what if you "proved", G:="This statement can't be proved", by assuming it could be proved and attaining a contradiction implying that it cannot be proved...

If this would work... It would seem the statement is neither true nor false, much like "this statement is a lie". What am I missing here?

$\endgroup$
8
  • $\begingroup$ Goedel's sentence says "there is no number which is the Goedel number of a proof of the statement whose number is the number you get by performing the following operations." When you perform the operations, it turns out to be the Goedel number of the Goedel sentence, but the sentence does not literally talk about itself; that's part of the meta-language. Moreover, "proof" refers to a formal proof within the system. The argument for why G would be "true but not provable", essentially what you give, is not a formal proof, and cannot be formalized within the language. $\endgroup$ Nov 8, 2022 at 15:19
  • 1
    $\begingroup$ @ArturoMagidin Could you specifically address what I was saying about proof by contradiction. As I understood that is a valid form of proof & if you assume that it is provable then as I understand you will attain a contradiction right? $\endgroup$
    – profPlum
    Nov 8, 2022 at 15:22
  • 1
    $\begingroup$ No one is saying proof by contradiction is not a valid form of proof. What I'm saying is that the argument you are making cannot be formalized within the language. It does not provide a formal proof of the Goedel statement: it shows that if the system is consistent then the statement cannot have a formal proof. The Goedel sentence doesn't say "This statement cannot be proven" (that's an incomplete, inaccurate gloss). It says "there is no number which is a formal proof for the following sentence." Not the same thing. $\endgroup$ Nov 8, 2022 at 15:24
  • 1
    $\begingroup$ The argument by contradiction ("If there were a formal proof of the Goedel statement within the theory, then the theory would be inconsistent, which contradicts our assumption that the system is consistent") is valid. It proves that there is no formal proof of the Goedel statement. The argument by contradiction (with some technical fixes and assumption, that one is a bit subtle) that if there is a formal proof of the negation of the statement then the system is inconsistent is also valid. That is what proves that G can neither be formally proven nor formally disproven. $\endgroup$ Nov 8, 2022 at 18:56
  • 1
    $\begingroup$ Note in particular that Goedel's Theorem is about formal provability, not about truth. Truth is a semantic notion (it depends on the meaning of the terms; it has to do with how you interpret the axioms, the model you are using). Formal provability is a syntactic notion: it depends on the rules for using and manipulating the symbols (the syntax of your theory), and not on the meaning of the symbols. The Completeness Theorem connects the two by saying that a statement is formally provable if and only if it is true in every interpretation of the theory. $\endgroup$ Nov 8, 2022 at 19:16

1 Answer 1

3
$\begingroup$

"But from my understanding he demonstrated that it is possible to encode the statement "This statement cannot be proved" using Gödel numbers..."

Not quite. What he did in effect was to encode the statement "This statement cannot be proved by proof system X" where X was a particular set of axioms and rules of deduction, which he could encode using precise arithmetical relationships. People had argued against paradoxes being a genuine problem by saying that English language was ambiguously defined and self-referential, and if you could make it precise enough the paradoxes would be avoided. That was the whole purpose of mathematics and logic. That it could be encoded in arithmetic told us we couldn't keep arithmetic and at the same time get rid of the paradoxes.

The caveat "This statement cannot be proved by proof system X" gives us a loophole to avoid the paradoxical self-contradiction. Any proof system apart from X that proves the statement does not give rise to a paradox. That's how humans can look at the statement and see intuitively that it is true, and not contradict themselves, because humans don't do proofs by the precise formal method Godel encoded.

However, the technique can be applied (informally, at least) to any prover, including humans. The statement "This statement cannot be proved by humans" could in principle be proved true by a non-human AI, but if a human could prove it then they would have proved something that was false, and would therefore be inconsistent, or they couldn't prove it and human proof is thus incomplete.

We can do stranger versions. "This statement cannot be proved on a Tuesday." "This statement cannot be proved by anyone wearing a hat." And so on. There is nothing special about human reasoning with regard to Godel-like statements. Indeed, it is widely known and entirely uncontroversial that informal human reasoning is both fallible and incomplete.

Interestingly, the same principle is the basis of a well-known puzzle - the problem of the unexpected hanging. A judge condemns a prisoner to death by hanging at dawn of some day of the following week, but stipulates that it should be a surprise; that the prisoner should not be able to deduce beforehand that he is to die the next day. This leads to an apparent contradiction - the prisoner cannot be hung on the last day, as he would know the day before, and hence he cannot be hung on the second to last day, and so on. He cannot be hung on any day! And so it comes as a complete surprise to him when he is hung on Tuesday. By setting conditions in the definition that refer to the evaluation process, we can make it possible to define quantities that can only be consistently evaluated in specific circumstances, or by some people and not others.

Of course, humans are not constrained to be consistent in proving or evaluating, which means we can usually figure it out anyway. But that doesn't pose any challenge to the idea behind Godel's theorem :- if our reasoning is consistent then it is incomplete. That we often reason inconsistently is not news - it's why we invented formal axiomatic mathematics in the first place!

$\endgroup$
1
  • $\begingroup$ Oh interesting! I guess Roger Penrose' related argument about 'AI being impossible' & 'physics being incapable of account for consciousness' kind of goes out the window when (like you said) all that necessary is for it to behave "inconsistently". That is clearly no problem for modern AI. $\endgroup$
    – profPlum
    Nov 8, 2022 at 21:51

You must log in to answer this question.

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