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 ${\mathsf {PA}}\vdash \Box C\to C$, then ${\mathsf {PA}}\vdash C$.

The deduction theorem says that if ${\mathsf {PA}}\cup \{H\}\vdash F$, then ${\mathsf {PA}}\vdash H\to F$.

Applying the deduction theorem to Löb's theorem gives us ${\mathsf {PA}}\vdash (\Box C\to C)\to C$.

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:

1. ${\mathsf {PA}}\vdash \Box L\leftrightarrow \Box (\Box L\to C)$
2. ${\mathsf {PA}}\vdash \Box C\to C$
3. ${\mathsf {PA}}\vdash \Box (\Box L\to C)\to (\Box \Box L\to \Box C)$
4. ${\mathsf {PA}}\vdash \Box L\to (\Box \Box L\to \Box C)$
5. ${\mathsf {PA}}\vdash \Box L\to \Box \Box L$
6. ${\mathsf {PA}}\vdash \Box L\to \Box C$
7. ${\mathsf {PA}}\vdash \Box L\to C$
8. ${\mathsf {PA}}\vdash \Box (\Box L\to C)$
9. ${\mathsf {PA}}\vdash \Box L$
10. ${\mathsf {PA}}\vdash C$