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

From Machinelearning
Jump to: navigation, search
(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 \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.

When translating to logic notation, it becomes obvious that the application of the deduction theorem is illegitimate, because we don't actually have \mathsf{PA} \cup \{\Box C \to C\} \vdash C. This is the initial answer that Larry D'Anna gives in comments.

But now, suppose we define \mathsf{PA}' := \mathsf{PA} \cup \{\Box C \to C\}, and walk through the proof of Löb's theorem for this new theory \mathsf{PA}'. Then we would obtain the following implication: if \mathsf{PA}' \vdash \Box C \to C, then \mathsf{PA}' \vdash C. But clearly, \mathsf{PA}' \vdash \Box C \to C since \Box C \to C is one of the axioms of \mathsf{PA}'. Therefore by modus ponens, we have \mathsf{PA}' \vdash C, i.e. \mathsf{PA}\cup\{\Box C \to C\} \vdash C. Now we can apply the deduction theorem to obtain \mathsf{PA} \vdash (\Box C \to C) \to C. This means that our "Löb's theorem" for \mathsf{PA}' 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:

  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

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

  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