Oscar_Cunningham comments on Löb’s theorem simply shows that Peano arithmetic cannot prove its own soundness

[Oscar_Cunningham]

Another good one is the spell ‘Assume for contradiction!’, which when you are trying to prove p gives you the lemma ¬p.