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

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 $P A ⊢ ◻ C \to C$ , then $P A ⊢ C$ .

The deduction theorem says that if $P A \cup {H} ⊢ F$ , then $P A ⊢ H \to F$ .

Applying the deduction theorem to Löb's theorem gives us $P A ⊢ (◻ 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 $P A \cup {◻ C \to C} ⊢ C$ . This is the initial answer that Larry D'Anna gives in comments.

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

$P A ⊢ ◻ L \leftrightarrow ◻ (◻ L \to C)$
$P A ⊢ ◻ C \to C$
$P A ⊢ ◻ (◻ L \to C) \to (◻ ◻ L \to ◻ C)$
$P A ⊢ ◻ L \to (◻ ◻ L \to ◻ C)$
$P A ⊢ ◻ L \to ◻ ◻ L$
$P A ⊢ ◻ L \to ◻ C$
$P A ⊢ ◻ L \to C$
$P A ⊢ ◻ (◻ L \to C)$
$P A ⊢ ◻ L$
$P A ⊢ C$

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

$P A' ⊢ ◻ L \leftrightarrow ◻ (◻ L \to C)$
$P A' ⊢ ◻ C \to C$
$P A' ⊢ ◻ (◻ L \to C) \to (◻ ◻ L \to ◻ C)$
$P A' ⊢ ◻ L \to (◻ ◻ L \to ◻ C)$
$P A' ⊢ ◻ L \to ◻ ◻ L$
$P A' ⊢ ◻ L \to ◻ C$
$P A' ⊢ ◻ L \to C$
$P A' ⊢ ◻ (◻ L \to C)$
$P A' ⊢ ◻ L$
$P A' ⊢ C$

@@ Line 31: / Line 31: @@
 # <math>\mathsf{PA} \vdash \Box L</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>