I think you've got one thing wrong. The statement 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 . 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 for some s.
What Löb's theorem says is that it can only do this for a trivial class of s, the ones that PA can prove outright. Obviously if PA can prove then it can prove (or indeed for any ). 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 , add ? 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: ; then . From , by necessitation , and so overall , that is . We have proven , by modus tollens .
Second, we can prove that soundness implies consistency without necessitation, by modus tollens and contradiction. Suppose . Further supposing clearly proves , so we reject the assumption, thus . Thus we prove , by modus tollens .
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.
If you told me to write down "PA can't prove its own soundness.", I would not write down Löb's theorem, I would write down "¬(PA ⊢ ∀p: Provable(p)→p)".
I would translate Löb's theorem as "In PA, when proving something, you get the lemma that it is provable for free.". Compare to "When proving a property for all natural numbers, you get the lemma that it holds for all smaller natural numbers for free."
You can't write down '∀p: Provable(p)→p' in PA, because in order to quantify over sentences we have to encode them as numbers (Gödel numbering).
We do have a formula Provable, such that when you substitute in the Gödel number p you get a sentence Provable(p) which is true if and only if the sentence p represents is provable. But we don't have a formula True, such that True(p) is true if and only if the sentence p represents is true. So the unadorned p in '∀p: Provable(p)→p' isn't possible. No such formula is possible since otherwise you could use diagonalization to construct the Liar Paradox: p⟷¬True(p) (Tarski's undefinability theorem).
What we can do is write down the sentence 'Provable(p)→p' for any particular Gödel number p. This is possible because when p is fixed we don't need True(p), we can just directly use the sentence p represents. I think of this as a restricted version of soundness: 'Soundness at p'. Then Löb's theorem tells us precisely which p PA is sound at. It's precisely the p which PA can prove.
Then apparently "PA can't prove its own soundness." is an even weaker true statement among the ones one might choose to remember :).
So, I might be getting something wrong, but why doesn't Löb's theorem imply that statement? A semi-formal argument, skipping some steps:
(Löb's theorem)
(Contraposition)
(e.g., 1 + 1 = 3)
(from 2)
(by change of quantifiers)
In PA, when proving something, you get the lemma that it is provable for free
As I understand it, this verbal statement can be translated to , or at least . The first is false[1] (Gödel's 1st incompleteness theorem), the second is not obviously related to Löb's theorem.
[1] also related to necessitation, a proof rule that substitutes for
Misunderstanding. I'm saying "In order to prove p, it suffices to prove □p→p.". Compare to complete induction.
I see, I misunderstood indeed.
What you wrote here is the literal statement of the theorem. It offers no extra understanding. I suppose you're right and I just wrote out a corollary, but I think the corollary is illuminating. I don't understand the comparison to induction in this comment or your previous one :(
We are trying to prove some statement p. When we're proving it for all pairs of real numbers x and y, the spell "Without loss of generality!" gives us the lemma "x<=y". When we're proving it for all natural numbers, the spell "Complete induction!" gives us the lemma "p holds for all smaller numbers". When we're working in PA, "Löb's Theorem!" gives us the lemma "Provable(p)".
Edit: And in general, math concepts are useful because of how they can be used. Memorize not things that are true, but things you can do. See this comment.
Another good one is the spell 'Assume for contradiction!', which when you are trying to prove p gives you the lemma ¬p.
EDIT: substituted "consistency" for "soundness". Thanks to Oscar_Cunningham for the correction!
Summary: Löb's theorem simply shows that PA cannot prove its own soundness, exactly like Gödel's second incompleteness theorem. I am very confident that this is not new, but it was new to me. Previously the theorem seemed circular and baffling.
Löb's theorem states that, in Peano Arithmetic or any system that contains it:
if PA⊢(Provable(p)→p), then PA⊢p.
I am using this notation instead of its more familiar modal logic rendition □(□p→p)→p because it yields the interpretation more easily.
The inner statement □p→p states that "if p is provable in PA, then it is a theorem of PA". It is the notion of soundness: that if the statement p can be proven, then it is true; that the PA system would not allow you to prove p if it were false.
With this in mind, we revise the statement of Löb's theorem, replacing p→q with the equivalent ¬p∨q:
PA⊢¬(Provable(p)→p)∨p.
That is: either p is true, or you cannot prove its soundness. You can thus only prove soundness of p (so (Provable(p)⟹p) is true) in settings where it is completely trivial, because you know that p is true already.
Even if Löb's theorem applied to only one false proposition p, it would show that PA is incomplete: it cannot determine its own soundness in this case. As it is stated, the situation is even worse: PA cannot determine its own soundness for any statement, unless soundness is trivial.