So it was that necessitation is outside of PA. Thank you! It seems to be assumed in modal logic (or at least a relevant modal logic) though. Which would imply that that modal logic assumes it is sound. It’s still a bit weird to me that Löb’s theorem is also true in that case.
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.
So it was that necessitation is outside of PA. Thank you! It seems to be assumed in modal logic (or at least a relevant modal logic) though. Which would imply that that modal logic assumes it is sound. It’s still a bit weird to me that Löb’s theorem is also true in that case.
The rule in modal logic is that we can get ⊢□p from ⊢p, not that we can get □p from p.
True:
False:
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.