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.
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:
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.
Peano Arthimetic is a first-order logic, so I’m reasonably certain the deduction theorem applies.