# Difference between revisions of "User:IssaRice/Computability and logic/Eliezer Yudkowsky's Löb's theorem puzzle"

From Machinelearning

(→Translating the Löb's theorem back to logic) |
|||

Line 2: | Line 2: | ||

current LW link: https://www.lesswrong.com/posts/ALCnqX6Xx8bpFMZq3/the-cartoon-guide-to-loeb-s-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 <math>\mathsf{PA} \vdash \Box C \to C</math>, then <math>\mathsf{PA} \vdash C</math>. | ||

+ | |||

+ | The deduction theorem says that if <math>\mathsf{PA} \cup \{H\} \vdash F</math>, then <math>\mathsf{PA} \vdash H \to F</math>. | ||

+ | |||

+ | Applying the deduction theorem to Löb's theorem gives us <math>\mathsf{PA} \vdash (\Box C \to C) \to C</math>. | ||

==Translating the Löb's theorem back to logic== | ==Translating the Löb's theorem back to logic== |

## Revision as of 03:19, 10 February 2019

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 .

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