Eliezer Yudkowsky comments on The Cartoon Guide to Löb’s Theorem

[Eliezer Yudkowsky]

Larry, interpret the smiley face as saying:

PA + (◻C → C) |-

Then the steps 1-10 of Lob’s proof would seem to take us from:

PA + (◻C → C) |- (◻C → C)

to

PA + (◻C → C) |- C

If this were the case, the deduction theorem would in fact come into play and give us:

PA |- (◻C → C) → C

So there must be at least one step of the reasoning 1-10 that does not apply. Which one and why?