I think you’ve got one thing wrong. The statement □p→p isn’t consistency, it’s a version of soundness. Consistency says that you can’t prove a contradiction, in symbols simply ¬□⊥. Whereas soundness is the stronger property that the things you prove are actually true, in symbols ∀p:□p→p. Of course first order logic can’t quantify over sentences, so you can’t even ask the question of whether PA can prove itself sound. But what you can ask is whether PA can prove itself sound for particular statements, i.e. whether it can prove □p→p for some ps.
What Löb’s theorem says is that it can only do this for a trivial class of ps, the ones that PA can prove outright. Obviously if PA can prove p then it can prove □p→p (or indeed q→p for any q). Löb’s theorem tells you that these obvious cases are the only ones for which you can prove PA sound.
I think you’re right, the statement is intuitively soundness, but I’m still confused. I would be very grateful if you could clear it up. Is “soundness → consistency” what you mean by stronger? If we can assume necessitation, soundness and consistency are equivalent, proof below.
Does that mean we cannot assume the necessitation proof rule, that is if ⊢p, add ⊢□p? This would be consistent with “PA cannot prove its own completeness”, the necessitation rule would imply that completeness is true.
First, we prove that consistency implies soundness by modus tollens. Suppose no soundness: ¬(□p→p); then □p∧¬p. From ¬p, by necessitation □¬p, and so overall □(p∧¬p), that is □⊥. We have proven ¬(□p→p)→□⊥, by modus tollens ¬□⊥→(□p→p).
Second, we can prove that soundness implies consistency without necessitation, by modus tollens and contradiction. Suppose □⊥. Further supposing □p→p clearly proves ⊥, so we reject the assumption, thus ¬(□p→p). Thus we prove □⊥→¬(□p→p), by modus tollens (□p→p)→¬□⊥.
Where did I go wrong? Is it the necessitation deduction rule? Is it that the necessitation deduction rule is valid, but cannot be used within a statement of 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:
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.
I think you’ve got one thing wrong. The statement □p→p isn’t consistency, it’s a version of soundness. Consistency says that you can’t prove a contradiction, in symbols simply ¬□⊥. Whereas soundness is the stronger property that the things you prove are actually true, in symbols ∀p:□p→p. Of course first order logic can’t quantify over sentences, so you can’t even ask the question of whether PA can prove itself sound. But what you can ask is whether PA can prove itself sound for particular statements, i.e. whether it can prove □p→p for some ps.
What Löb’s theorem says is that it can only do this for a trivial class of ps, the ones that PA can prove outright. Obviously if PA can prove p then it can prove □p→p (or indeed q→p for any q). Löb’s theorem tells you that these obvious cases are the only ones for which you can prove PA sound.
I think you’re right, the statement is intuitively soundness, but I’m still confused. I would be very grateful if you could clear it up. Is “soundness → consistency” what you mean by stronger? If we can assume necessitation, soundness and consistency are equivalent, proof below.
Does that mean we cannot assume the necessitation proof rule, that is if ⊢p, add ⊢□p? This would be consistent with “PA cannot prove its own completeness”, the necessitation rule would imply that completeness is true.
First, we prove that consistency implies soundness by modus tollens. Suppose no soundness: ¬(□p→p); then □p∧¬p. From ¬p, by necessitation □¬p, and so overall □(p∧¬p), that is □⊥. We have proven ¬(□p→p)→□⊥, by modus tollens ¬□⊥→(□p→p).
Second, we can prove that soundness implies consistency without necessitation, by modus tollens and contradiction. Suppose □⊥. Further supposing □p→p clearly proves ⊥, so we reject the assumption, thus ¬(□p→p). Thus we prove □⊥→¬(□p→p), by modus tollens (□p→p)→¬□⊥.
Where did I go wrong? Is it the necessitation deduction rule? Is it that the necessitation deduction rule is valid, but cannot be used within a statement of 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.