Oscar_Cunningham comments on Löb’s theorem simply shows that Peano arithmetic cannot prove its own soundness

[Oscar_Cunningham]

The rule in modal logic is that we can get ⊢□p from ⊢p, not that we can get □p from p.

True:

If PA proves p, then PA proves that PA proves p.

False:

If p, then PA proves p.

EDIT: Maybe it would clarify to say that ‘⊢p’ and ‘□p’ both mean ‘PA (or whichever theory) can prove p’, but ‘⊢’ is used when talking about PA, whereas ‘□’ is used when talking within PA.