From our vantage point of ZFC, we can see that PA is in fact consistent. But we know that PA can’t prove its own consistency or inconsistency. So the classic example of a system which is consistent but unsound is PA + ¬Con(PA). This system is consistent since deriving a contradiction in it would amount to a proof by contradiction of consistency in PA, which we know is impossible. But it’s unsound since it falsely believes that PA is not consistent.
Your proof of ‘consistency → soundness’ goes wrong in the following way:
Suppose no soundness: ¬(□p→p); then □p∧¬p.
This is correct. But to be more clear, a theory being unsound would mean that there was some p for which the sentence ‘□p∧¬p’ was true, not that there was some p for which the sentence ‘□p∧¬p’ was provable in that theory. So then in the next line
From ¬p, by necessitation □¬p
we can’t apply necessitation, because we don’t know that our theory proves ¬p, only that p is false.
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.
From our vantage point of ZFC, we can see that PA is in fact consistent. But we know that PA can’t prove its own consistency or inconsistency. So the classic example of a system which is consistent but unsound is PA + ¬Con(PA). This system is consistent since deriving a contradiction in it would amount to a proof by contradiction of consistency in PA, which we know is impossible. But it’s unsound since it falsely believes that PA is not consistent.
Your proof of ‘consistency → soundness’ goes wrong in the following way:
This is correct. But to be more clear, a theory being unsound would mean that there was some p for which the sentence ‘□p∧¬p’ was true, not that there was some p for which the sentence ‘□p∧¬p’ was provable in that theory. So then in the next line
we can’t apply necessitation, because we don’t know that our theory proves ¬p, only that p is false.
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.