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.
Löb’s theorem simply shows that Peano arithmetic cannot prove its own soundness
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.