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

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


But now, suppose we define <math>\mathsf{PA}' := \mathsf{PA} \cup \{\Box C \to C\}</math>, and walk through the proof of Löb's theorem for this new theory <math>\mathsf{PA}'</math>. Then we would obtain the following implication: if <math>\mathsf{PA}' \vdash \Box C \to C</math>, then <math>\mathsf{PA}' \vdash C</math>. But clearly, <math>\mathsf{PA}' \vdash \Box C \to C</math> since <math>\Box C \to C</math> is one of the axioms of <math>\mathsf{PA}'</math>. Therefore by modus ponens, we have <math>\mathsf{PA}' \vdash C</math>, i.e. <math>\mathsf{PA}\cup\{\Box C \to C\} \vdash C</math>. Now we can apply the deduction theorem to obtain <math>\mathsf{PA} \vdash (\Box C \to C) \to C</math>. This means that our "Löb's theorem" for <math>\mathsf{PA}'</math> must be incorrect, and somewhere in the ten-step proof is an error.
But now, suppose we define <math>\mathsf{PA}' := \mathsf{PA} \cup \{\Box C \to C\}</math>, and walk through the proof of Löb's theorem for this new theory <math>\mathsf{PA}'</math>. Then we would obtain the following implication: if <math>\mathsf{PA}' \vdash \Box C \to C</math>, then <math>\mathsf{PA}' \vdash C</math>. But clearly, <math>\mathsf{PA}' \vdash \Box C \to C</math> since <math>\Box C \to C</math> is one of the axioms of <math>\mathsf{PA}'</math>. Therefore by modus ponens, we have <math>\mathsf{PA}' \vdash C</math>, i.e. <math>\mathsf{PA}\cup\{\Box C \to C\} \vdash C</math>. Now we can apply the deduction theorem to obtain <math>\mathsf{PA} \vdash (\Box C \to C) \to C</math>. This means that our "Löb's theorem" for <math>\mathsf{PA}'</math> must be incorrect (note: the proof ''is'' correct for <math>\mathsf{PA}</math>; it's just incorrect for <math>\mathsf{PA}'</math>), and somewhere in the ten-step proof is an error.


==Translating the Löb's theorem back to logic==
==Translating the Löb's theorem back to logic==

Revision as of 03:34, 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 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}'} . Then we would obtain the following implication: 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 C} . But clearly, 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} 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 \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}'} . Therefore by modus ponens, we have 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} , i.e. 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}\cup\{\Box C \to C\} \vdash C} . Now we can apply the deduction theorem to obtain 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) \to C} . This means that our "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}'} must be incorrect (note: the proof is correct 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}} ; it's just incorrect 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}'} ), 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. 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)}
  2. 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}
  3. 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)}
  4. 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)}
  5. 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}
  6. 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}
  7. 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}
  8. 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)}
  9. 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}
  10. 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.

  1. 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)}
  2. 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}
  3. 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)}
  4. 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)}
  5. 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}
  6. 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}
  8. 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)}
  9. 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}
  10. 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}
Retrieved from "https://machinelearning.subwiki.org/w/index.php?title=User:IssaRice/Computability_and_logic/Eliezer_Yudkowsky%27s_Löb%27s_theorem_puzzle&oldid=1596"