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

Revision as of 06: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

This page gives spoilers for the puzzle!

This pages states the puzzle and gives the solution.

Notation

Precedence:

$\Box$ has high precedence, so e.g. $\Box C\to C$ means $(\Box C)\to C$ , and $\Box \Box L\to \Box C$ means $(\Box \Box L)\to (\Box C)$ .
$\vdash$ is a metalogical notion and has low precedence, so ${\mathsf {PA}}\vdash \Box C\to C$ means ${\mathsf {PA}}\vdash (\Box C\to C)$ .

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 (note: the proof is correct for ${\mathsf {PA}}$ , which is why Löb's theorem is a theorem; it's just incorrect for ${\mathsf {PA}}'$ ), 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:

${\mathsf {PA}}\vdash \Box L\leftrightarrow \Box (\Box L\to C)$ by construction of $L$
${\mathsf {PA}}\vdash \Box C\to C$ by hypothesis
${\mathsf {PA}}\vdash \Box (\Box L\to C)\to (\Box \Box L\to \Box C)$
${\mathsf {PA}}\vdash \Box L\to (\Box \Box L\to \Box C)$
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA} \vdash \Box L \to \Box \Box L}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA} \vdash \Box L \to \Box C}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA} \vdash \Box L \to C}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA} \vdash \Box(\Box L \to C)}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA} \vdash \Box L}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA} \vdash C}

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

We now repeat the proof of Löb's theorem for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}' := \mathsf{PA} \cup \{\Box C \to C\}} to see where the error is.

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}' \vdash \Box L \leftrightarrow \Box(\Box L \to C)} by construction of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle L}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}' \vdash \Box C \to C} because Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Box C \to C} is one of the axioms of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}'}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}' \vdash \Box(\Box L \to C) \to (\Box \Box L \to \Box C)} instance of A3
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}' \vdash \Box L \to (\Box \Box L \to \Box C)}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}' \vdash \Box L \to \Box \Box L}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}' \vdash \Box L \to \Box C}
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}' \vdash \Box L \to C}

So far, everything is fine. But can we assert Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}' \vdash \Box(\Box L \to C)} ? For Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}} , we had the following:

A1: For each sentence Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X} , if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}\vdash X} then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA} \vdash \Box X}

We need the following:

A1′: For each sentence Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X} , if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}'\vdash X} then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}' \vdash \Box X}

Since Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}'} has more axioms than Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}} , we know that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}'} can prove everything that ${\mathsf {PA}}$ can. Thus, compared to A1, both the antecedent and consequent of A1′ are weaker, so A1′ does not necessarily follow from A1.

Suppose we take Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X} in A1′ to be Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Box C \to C} . Then we obtain

If Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}'\vdash \Box C \to C} then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}' \vdash \Box (\Box C \to C)}

Other ways we might try to get step 8 to work:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}' \vdash X \to \Box X}
if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X} , then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA} \vdash X} -- i think this is the one about which Larry says "ARGH WHAT ARE YOU DOING". Or maybe he means "if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Delta \vdash X} , then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Delta \vdash \Box X} " for arbitrary Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Delta} .
- Now one might wonder, why is Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Delta=\mathsf{PA}} so special?

But can we prove that we can never get step 8 for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathsf{PA}'} ? Well, this is exactly what the puzzle statement does -- it assumes the proof goes through, and derives an absurdity! (? actually, i'm not sure this is actually a contradiction. If we assume PA is consistent, then it seems to be a contradiction. I think this is the point nate soares and alex flint are trying to make in the comments. but we can re-word the puzzle to say one should find the first error.)

@@ Line 73: / Line 73: @@
 * <math>\mathsf{PA}' \vdash X \to \Box X</math>
 * if <math>X</math>, then <math>\mathsf{PA} \vdash X</math> -- i think this is the one about which Larry says "ARGH WHAT ARE YOU DOING". Or maybe he means "if <math>\Delta \vdash X</math>, then <math>\Delta \vdash \Box X</math>" for arbitrary <math>\Delta</math>.
+** Now one might wonder, why is <math>\Delta=\mathsf{PA}</math> so special?
 But can we ''prove'' that we can never get step 8 for <math>\mathsf{PA}'</math>? Well, this is exactly what the puzzle statement does -- it assumes the proof goes through, and derives an absurdity! (? actually, i'm not sure this is actually a contradiction. If we assume PA is consistent, then it seems to be a contradiction. I think this is the point nate soares and alex flint are trying to make in the comments. but we can re-word the puzzle to say one should find the ''first'' error.)