Sanity check: If I'm understanding Eleizer and D'Anna correctly, step 8 is valid in PA but not in classical (= first order?) logic. The deduction theorem only applies to proofs in classical logic, therefore this part:

"Applying the Deduction Theorem to Löb's Theorem gives us, for all C:

((◻C)->C)->C"

is incorrect; you can't use the deduction theorem on Lob's Theorem. Everything after that is invalidated, including 2=1.

Is that more or less the point here? I have a good head for math but I'm not formally trained, so I'm trying to be sure I actually understand this instead of just thinking I understand it.

Incidentally: Godel's Theorem inspired awe when I was first exposed to it, and now Lob's has done the same. I actually first read this post months ago, but it's only going back to it after chasing links from a future sequence that I think I finally get it.