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

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:

• $◻$ has high precedence, so e.g. $◻C\to C$ means $(◻C)\to C$, and $◻◻L\to ◻C$ means $(◻◻L)\to (◻C)$.
• $⊢$ is a metalogical notion and has low precedence, so $\mathsf{P}\mathsf{A}⊢◻C\to C$ means $\mathsf{P}\mathsf{A}⊢(◻C\to C)$.

Translating the puzzle using logic notation

Löb's theorem shows that if $\mathsf{P}\mathsf{A}⊢◻C\to C$, then $\mathsf{P}\mathsf{A}⊢C$.

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

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

But now, suppose we define $\mathsf{P}\mathsf{A}\text{'}:=\mathsf{P}\mathsf{A}\cup \{◻C\to C\}$, and walk through the proof of Löb's theorem for this new theory $\mathsf{P}\mathsf{A}\text{'}$. Then we would obtain the following implication: if $\mathsf{P}\mathsf{A}\text{'}⊢◻C\to C$, then $\mathsf{P}\mathsf{A}\text{'}⊢C$. But clearly, $\mathsf{P}\mathsf{A}\text{'}⊢◻C\to C$ since $◻C\to C$ is one of the axioms of $\mathsf{P}\mathsf{A}\text{'}$. Therefore by modus ponens, we have $\mathsf{P}\mathsf{A}\text{'}⊢C$, i.e. $\mathsf{P}\mathsf{A}\cup \{◻C\to C\}⊢C$. Now we can apply the deduction theorem to obtain $\mathsf{P}\mathsf{A}⊢(◻C\to C)\to C$. This means that our "Löb's theorem" for $\mathsf{P}\mathsf{A}\text{'}$ must be incorrect (note: the proof is correct for $\mathsf{P}\mathsf{A}$, which is why Löb's theorem is a theorem; it's just incorrect for $\mathsf{P}\mathsf{A}\text{'}$), 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{P}\mathsf{A}⊢◻L\leftrightarrow ◻(◻L\to C)$ by construction of $L$
2. $\mathsf{P}\mathsf{A}⊢◻C\to C$ by hypothesis
3. $\mathsf{P}\mathsf{A}⊢◻(◻L\to C)\to (◻◻L\to ◻C)$
4. $\mathsf{P}\mathsf{A}⊢◻L\to (◻◻L\to ◻C)$
5. $\mathsf{P}\mathsf{A}⊢◻L\to ◻◻L$
6. $\mathsf{P}\mathsf{A}⊢◻L\to ◻C$
7. $\mathsf{P}\mathsf{A}⊢◻L\to C$
8. $\mathsf{P}\mathsf{A}⊢◻(◻L\to C)$
9. $\mathsf{P}\mathsf{A}⊢◻L$
10. $\mathsf{P}\mathsf{A}⊢C$

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

We now repeat the proof of Löb's theorem for $\mathsf{P}\mathsf{A}\text{'}:=\mathsf{P}\mathsf{A}\cup \{◻C\to C\}$ to see where the error is.

1. $\mathsf{P}\mathsf{A}\text{'}⊢◻L\leftrightarrow ◻(◻L\to C)$ by construction of $L$
2. $\mathsf{P}\mathsf{A}\text{'}⊢◻C\to C$ because $◻C\to C$ is one of the axioms of $\mathsf{P}\mathsf{A}\text{'}$
3. $\mathsf{P}\mathsf{A}\text{'}⊢◻(◻L\to C)\to (◻◻L\to ◻C)$ instance of A3
4. $\mathsf{P}\mathsf{A}\text{'}⊢◻L\to (◻◻L\to ◻C)$
5. $\mathsf{P}\mathsf{A}\text{'}⊢◻L\to ◻◻L$
6. $\mathsf{P}\mathsf{A}\text{'}⊢◻L\to ◻C$
7. $\mathsf{P}\mathsf{A}\text{'}⊢◻L\to C$

So far, everything is fine. But can we assert $\mathsf{P}\mathsf{A}\text{'}⊢◻(◻L\to C)$? For $\mathsf{P}\mathsf{A}$, we had the following:

A1: For each sentence $X$, if $\mathsf{P}\mathsf{A}⊢X$ then $\mathsf{P}\mathsf{A}⊢◻X$

We need the following:

A1′: For each sentence $X$, if $\mathsf{P}\mathsf{A}\text{'}⊢X$ then $\mathsf{P}\mathsf{A}\text{'}⊢◻X$

Since $\mathsf{P}\mathsf{A}\text{'}$ has more axioms than $\mathsf{P}\mathsf{A}$, we know that $\mathsf{P}\mathsf{A}\text{'}$ can prove everything that $\mathsf{P}\mathsf{A}$ 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 $X$ in A1′ to be $◻C\to C$. Then we obtain

If $\mathsf{P}\mathsf{A}\text{'}⊢◻C\to C$ then $\mathsf{P}\mathsf{A}\text{'}⊢◻(◻C\to C)$

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

• $\mathsf{P}\mathsf{A}\text{'}⊢X\to ◻X$
• if $X$, then $\mathsf{P}\mathsf{A}⊢X$ -- i think this is the one about which Larry says "ARGH WHAT ARE YOU DOING". Or maybe he means "if $\mathrm{\Delta }⊢X$, then $\mathrm{\Delta }⊢◻X$" for arbitrary $\mathrm{\Delta }$.
  • Now one might wonder, why is $\mathrm{\Delta }=\mathsf{P}\mathsf{A}$ so special? I think this happens because $◻$ is the provability predicate of $\mathsf{P}\mathsf{A}$ and not some other theory. In particular, if $\mathrm{\Delta }\supseteq \mathsf{P}\mathsf{A}$, then if $\mathrm{\Delta }⊢X$ we only know the weaker statement that $\mathrm{\Delta }$ proves $X$, not that $\mathsf{P}\mathsf{A}$ proves it. So we shouldn't be able to prove that $\mathrm{\Delta }$ can prove $◻X$. What if $\mathrm{\Delta }\subseteq \mathsf{P}\mathsf{A}$? Then I think we are in a better position. e.g. if $\mathrm{\Delta }=\mathsf{Q}$, then I think $\mathsf{Q}$ can still represent the provability predicate of $\mathsf{P}\mathsf{A}$ (?) so then we have $\mathsf{Q}⊢◻X$. (this part might be wrong)

But can we prove that we can never get step 8 for $\mathsf{P}\mathsf{A}\text{'}$? 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.)

Other questions to answer

• does $◻$ in $\mathsf{P}\mathsf{A}\text{'}$ still mean provability about $\mathsf{P}\mathsf{A}$, or about itself?
• are we removing a layer or adding one?
• can't $\mathsf{P}\mathsf{A}\text{'}$ prove everything $\mathsf{P}\mathsf{A}$ can? yes, but this doesn't mean we can substitute implications automatically because the consequent also gets stronger