User:IssaRice/Computability and logic/Eliezer Yudkowsky's Löb's theorem puzzle
original link: https://web.archive.org/web/20160319050228/http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%B6bs_theorem/
current LW link: https://www.lesswrong.com/posts/ALCnqX6Xx8bpFMZq3/the-cartoon-guide-to-loeb-s-theorem
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, and somewhere in the ten-step proof is an error.
Translating the Löb's theorem back to logic
http://yudkowsky.net/assets/44/LobsTheorem.pdf
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: