User:IssaRice/Computability and logic/Eliezer Yudkowsky's Löb's theorem puzzle
This page gives spoilers for the puzzle!
This pages states the puzzle and gives the solution.
- has high precedence, so e.g. means , and means .
- is a metalogical notion and has low precedence, so means .
Translating the puzzle using logic notation
Löb's theorem shows that if , then .
The deduction theorem says that if , then .
Applying the deduction theorem to Löb's theorem gives us .
When translating to logic notation, it becomes obvious that the application of the deduction theorem is illegitimate, because we don't actually have . This is the initial answer that Larry D'Anna gives in comments.
But now, suppose we define , and walk through the proof of Löb's theorem for this new theory . Then we would obtain the following implication: if , then . But clearly, since is one of the axioms of . Therefore by modus ponens, we have , i.e. . Now we can apply the deduction theorem to obtain . This means that our "Löb's theorem" for must be incorrect (note: the proof is correct for , which is why Löb's theorem is a theorem; it's just incorrect for ), and somewhere in the ten-step proof is an error.
Translating the Löb's theorem back to logic
Since the solution to the puzzle refers back to the proof of Löb's theorem, we first translate the proof from the cartoon version back to logic:
- by construction of
- by hypothesis
Repeating the proof of Löb's theorem for modified theory
We now repeat the proof of Löb's theorem for to see where the error is.
- by construction of
- because is one of the axioms of
- instance of A3
So far, everything is fine. But can we assert ? For , we had the following:
- A1: For each sentence , if then
We need the following:
- A1′: For each sentence , if then
Since has more axioms than , we know that can prove everything that can. Thus, compared to A1, both the antecedent and consequent of A1′ are weaker, so A1′ does not necessarily follow from A1.
Suppose we take in A1′ to be . Then we obtain
- If then
Other ways we might try to get step 8 to work:
- if , then -- i think this is the one about which Larry says "ARGH WHAT ARE YOU DOING". Or maybe he means "if , then " for arbitrary .
- Now one might wonder, why is so special? I think this happens because is the provability predicate of and not some other theory. In particular, if , then if we only know the weaker statement that proves , not that proves it. So we shouldn't be able to prove that can prove . What if ? Then I think we are in a better position. e.g. if , then I think can still represent the provability predicate of (?) so then we have . (this part might be wrong)
But can we prove that we can never get step 8 for ? Well, this is exactly what the puzzle statement does -- it assumes the proof goes through, and derives an absurdity! (? actually, i'm not sure this is actually a contradiction. If we assume PA is consistent, then it seems to be a contradiction. I think this is the point nate soares and alex flint are trying to make in the comments. but we can re-word the puzzle to say one should find the first error.)
Other questions to answer
- does in still mean provability about , or about itself?
- are we removing a layer or adding one?
- can't prove everything can? yes, but this doesn't mean we can substitute implications automatically because the consequent also gets stronger