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

SamEisenstat 21 Apr 2020 7:03 UTC
7 points
0
*I* think that there’s a flaw in the argument.
I could elaborate, but maybe you want to think about this more, so for now I’ll just address your remark about $\neg □ C \to C$ , where $C$ is refutable. If we assume that $\neg □ C \to C$ , then, since $C$ is false, $\neg □ C$ must be false, so $□ C$ must be true. That is, you have proven that PA proves $□ C$ , that is, since $C$ is contradictory, PA proves its own inconsistency. You’re right that this is compatible with PA being consistent—PA may be consistent but prove its own inconsistency—but this should still be worrying.
- jpulgarin 19 May 2020 6:27 UTC
  2 points
  0
  Parent
  Thanks Sam. I thought about this some more and realized where I went wrong—I was applying the deduction theorem incorrectly (as other comments in this thread have pointed out).
  By the way, when you say that PA proves its own inconsistency, do you mean that $P A ⊢ □ (\neg C o n (P A))$ or that $P A ⊢ \neg C o n (P A)$ ? From your reasoning I agree that if we assume $\neg □ C \to C$ then we can arrive at $P A ⊢ □ C$ and $P A ⊢ □ (\neg C)$ , from which we can conclude that $P A ⊢ □ (\neg C o n (P A))$ . If you meant that $P A ⊢ \neg C o n (P A)$ though, could you explain how you arrived at that?