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 PA⊢□(¬Con(PA)) or that PA⊢¬Con(PA)? From your reasoning I agree that if we assume ¬□C→C then we can arrive at PA⊢□C and PA⊢□(¬C), from which we can conclude that PA⊢□(¬Con(PA)). If you meant that PA⊢¬Con(PA) though, could you explain how you arrived at that?
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 PA⊢□(¬Con(PA)) or that PA⊢¬Con(PA)? From your reasoning I agree that if we assume ¬□C→C then we can arrive at PA⊢□C and PA⊢□(¬C), from which we can conclude that PA⊢□(¬Con(PA)). If you meant that PA⊢¬Con(PA) though, could you explain how you arrived at that?