User:IssaRice/Computability and logic/Eliezer Yudkowsky's Löb's theorem puzzle: Difference between revisions
(Created page with "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/...") |
No edit summary |
||
| 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 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: | |||
# <math>\mathsf{PA} \vdash \Box L \leftrightarrow \Box(\Box L \to C)</math> | |||
# <math>\mathsf{PA} \vdash \Box C \to C</math> | |||
# <math>\mathsf{PA} \vdash \Box(\Box L \to C) \to (\Box \Box L \to \Box C)</math> | |||
# <math>\mathsf{PA} \vdash \Box L \to (\Box \Box L \to \Box C)</math> | |||
# <math>\mathsf{PA} \vdash \Box L \to \Box \Box L</math> | |||
# <math>\mathsf{PA} \vdash \Box L \to \Box C</math> | |||
# <math>\mathsf{PA} \vdash \Box L \to C</math> | |||
# <math>\mathsf{PA} \vdash \Box(\Box L \to C)</math> | |||
# <math>\mathsf{PA} \vdash \Box\Box L</math> | |||
# <math>\mathsf{PA} \vdash \Box C</math> | |||
Revision as of 03:02, 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 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:
