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.
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.