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.

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.