Thanks for this. Just curious, is there a constructive argument for the lemma, such that it also holds for intuitionistic logic where proof by contradiction is not allowed?This explanation is just the sketch of an argument by contradiction for the Gödel-Carnap's diagonal lemma — alcontali
Just curious, is there a constructive argument for the lemma, such that it also holds for intuitionistic logic where proof by contradiction is not allowed? — aletheist
not S ↔ K(%(not S))
For the sake of the argument, let's now rename "not S" to "P":
P ↔ K(%P)
Look at that! We now have a sentence P that has the property of being heavy, even though K, the heaviness predicate, always returns false! How is that possible? — alcontali
P ↔ not provable(%P) — alcontali
we only know that there is some false proposition that has the same truth value as a predicate function that always returns false, which... duh. — Pfhorrest
I don’t see how any conclusions can be drawn from that to more general statements about predicate functions that sometimes return true or sentences that are true. — Pfhorrest
We could trivially invert the truth values and say that any true sentence has any predicate that always returns true — Pfhorrest
which just says that in a system in which nothing is provable, any true sentence is not provable, which is again trivial. — Pfhorrest
You actually did not describe the lemma ... What is the meaningfulness of talking about two somethings none of us understands, and none of us has any comprehension or concept of? — god must be atheist
So we don't know what the problem is, and we don't know its solution. — god must be atheist
It is just a game and you must hit the diagonal.
[(false,false)(false,true)(true,false)(true,true)][(false,false)(true,false)(false,true)(true,true)]
The first example predicate, "isEven", will return true if a number is even and false if it is odd.
In this game, you can use whatever logic sentence you want, but if it is true, its number must be even. If it is false, then its number must be odd. You must stay on the diagonal! — alcontali
So, no, you cannot just say, "you do not understand it". — alcontali
7. If I am too stupid to understand this, please tell me now, outright, so I shall cease and desist, and not bother you with questions. — god must be atheist
You haven't told us how to determine the number of a sentence. And once you give us the rule to determine the number of a sentence (I imagine it's ordinal numbers, not cardinals), then... — god must be atheist
Especially its proof is considered to be incomprehensible. That is a problem because both Gödel's first incompleteness theorem and Tarski's undefinability theorem trivially follow from this lemma. Let's attempt to come up with a more intuitive explanation anyway. — alcontali
Third step. Let's now specify a property that could not possibly apply to any sentence
Let's define K(%M) = false. Say that K means "heavy". (It could mean anything, really). There is no number or associated sentence that is "heavy" because K always returns false. We just do not want a heavy sentence in our system. Seriously, we are trying to shoehorn the situation here to prevent anything from being provably heavy. — alcontali
Look at that! We now have a sentence P that has the property of being heavy, even though K, the heaviness predicate, always returns false! How is that possible? — alcontali
3. utf8( 1=1 or 99=99 or 0=0 ) = 496149321111143257576157573211111432486148 ⇐⇐ BINGO!
Example 3 is true and even. So, it is a solution, i.e. a witness to the lemma. Just for the sake of the argument, let's now try to find an arbitrary false sentence that is odd:
4. utf8( 0=1 ) = 486149 ⇐⇐ BINGO!
Example 4 is false and odd. So, it is also a solution, i.e. a witness to the lemma. — alcontali
So, you can also play this game with the "isProvable" predicate, but the really interesting game is with the "isNotProvable" predicate, because as soon as you win the game by finding a true sentence, you will have a true sentence that also "isNotProvable", and that is considered to be an astonishing result in metalogic and metamathematics. — alcontali
They express their (utter) dislike for this lemma. — alcontali
So would this show that some true sentences are not provable, or just that those "true" sentences are problematic in some way, similar to the liar sentence or the above "heavy" sentences? — Andrew M
So would this show that some true sentences are not provable, or just that those "true" sentences are problematic in some way, similar to the liar sentence or the above "heavy" sentences? — Andrew M
Again, maybe my memory is playing tricks on me. So I ask you, instead of accusing you: did you reword the opening post? — god must be atheist
No. I stopped drafting it after probably half an hour or so, and then left it like that. — alcontali
Well, the term "heavy" was probably a bad choice. I couldn't think of a some good predicate, because the literature pretty much never mentions one. It needs to be something calculable true or false about a sentence. The literature typically says something like: "The sentence S has property K". Any idea of what could be a good example for K? — alcontali
Well, since "heavy" is just an arbitrary choice, I wouldn't worry about that. As long as you can calculate the property from a number, it should be ok. For example: "the face is green" should probably work better, because a face can be represented as a number, and figuring out that is green, is just a calculation on its bits and bytes. So, the diagonal lemma says that it should always be possible to construct a face that is green, but also one that is not green. — alcontali
I think either something about the form of the sentence (e.g., HasAnEvenNumberOfLetters) — Andrew M
IsProvable doesn't seem to meet that criteria since it depends on the meaning of the sentence. — Andrew M
But "the face is green" is not a predicate. It's fine as a sentence however (with a Godel number). — Andrew M
So, counting letters in utf8 is just another numbers game. — alcontali
It is also just another numbers game. Say that "12>3" is a simple theorem in arithmetic. Then, the following sequence of sentences is one possible proof:
1) 12>3
2) 12-3>3-3
3) 9>0
In 3) we hit axiom 15 in the equivalent axiomatization: i.e. zero is the minimum element.
So, now we convert the theorem to a number:
utf8("12>3")=49506251
utf8("12>3 ; 12-3>3-3 ; 9>0")=495062513259324950455162514551325932576248
So, now we can say that theorem 49506251 is provable because it is associated to another number. 495062513259324950455162514551325932576248, which is its proof. Therefore, the predicate isProvable(49506251) results in true. — alcontali
Still, in an idealized world the "isProvable" predicate can really be implemented. — alcontali
From there on, it will still not be able to avoid hitting the diagonal lemma: there exists a true sentence which "isNotProvable". — alcontali
Still, in an idealized world the "isProvable" predicate can really be implemented — alcontali
Meaning that ideally every true statement has a corresponding proof and every false statement has no corresponding proof (or perhaps a corresponding disproof)? — Andrew M
And is that the diagonal? (i.e., false/not provable, true/provable) — Andrew M
OK, how does this part work? — Andrew M
The diagonal lemma says that it is always possible for any arbitrary property about numbers to hit the diagonal. This means that you can always find a true sentence that has the property but also a false sentence that does not have the property. — alcontali
This is the part I don't understand. How is this proved? — Andrew M
Take any property, e.g. isLargeNumber. Say that isLargeNumber is true for numbers above 10^20, and false for numbers that are smaller.
Now, the diagonal lemma says that you can always find a true sentence for which isLargeNumber is true. You can also always find a false sentence for which isLargeNumber is false. — alcontali
But how about the property isNegativeNumber? That property will never be true. — Andrew M
OK, so to go back to the third step in your initial post, K could be isNegative. And so isNegative(%M) is false. Then, per the fourth step, any false sentence will have the property isNegative. — Andrew M
Given the above, it seems that there doesn't have to be a true statement that is not provable. There could instead be a false statement that is provable. So it would be a choice between incompleteness and unsoundness? — Andrew M
OK, so my understanding is that one sentence that hits (true,true) for isNotProvable is the sentence that asserts that it is itself not provable. How is that expressed as a mathematical sentence? — Andrew M
Also, why is it thought to be true? — Andrew M
Is it simply that assuming that it is provable leads to contradiction? — Andrew M
It is just about the fact that we can define the "isNotProvable" predicate as a number predicate. — alcontali
If no true but unprovable X has been found to satisfy "X ↔ isNotProvable(%X)", then why should we consider it to be a satisifiable definition? — Andrew M
Also, would "X ↔ isNotTrue(%X)" be considered a satisifiable definition? I assume not, but that then raises the question of the criteria for judging that a definition is satisfiable. — Andrew M
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.