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.
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 p→□p, or at least □p→□□p. 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 PA⊢p for PA⊢□p
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.
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:
1.∀p(PA⊢(Prov(p)→p))→(PA⊢p)) (Löb’s theorem)
2.∀p(¬(PA⊢p)→¬(PA⊢(Prov(p)→p))) (Contraposition)
3.∃p¬(PA⊢p) (e.g., 1 + 1 = 3)
4.∃p¬(PA⊢(Prov(p)→p)) (from 2)
5.¬∀p(PA⊢(Prov(p)→p)) (by change of quantifiers)
Yes, but 3 is a one-way street. You should remember the theorem, not the corollary.
As I understand it, this verbal statement can be translated to p→□p, or at least □p→□□p. 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 PA⊢p for PA⊢□p
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.