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

(→Translating the puzzle using logic notation) |
|||

Line 31: | Line 31: | ||

# <math>\mathsf{PA} \vdash \Box L</math> | # <math>\mathsf{PA} \vdash \Box L</math> | ||

# <math>\mathsf{PA} \vdash C</math> | # <math>\mathsf{PA} \vdash C</math> | ||

+ | |||

+ | ==Repeating the proof of Löb's theorem for modified theory== | ||

+ | |||

+ | # <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 L</math> | ||

+ | # <math>\mathsf{PA}' \vdash C</math> |

## Revision as of 03:33, 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 .

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: