# 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 (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

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:

## 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 definition of
- because is one of the axioms of

So far, everything is fine. But can we assert ? For , we had the following:

- A1: For each , if then