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

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.