Löb's theorem

We trust Peano Arith­metic to cor­rectly cap­ture cer­tain fea­tures of the stan­dard model of ar­ith­metic. Fur­ther­more, we know that Peano Arith­metic is ex­pres­sive enough to talk about it­self in mean­ingful ways. So it would cer­tainly be great if Peano Arith­metic as­serted what now is an in­tu­ition: that ev­ery­thing it proves is cer­tainly true.

In for­mal no­ta­tion, let \(Prv\) stand for the stan­dard prov­abil­ity pred­i­cate of \(PA\). Then, \(Prv(T)\) is true if and only if there is a proof from the ax­ioms and rules of in­fer­ence of \(PA\) of \(T\). Then what we would like \(PA\) to say is that \(Prv(S)\implies S\) for ev­ery sen­tence \(S\).

But alas, \(PA\) suffers from a prob­lem of self-trust.

Löb’s the­o­rem states that if \(PA\vdash Prv(S)\implies S\) then \(PA\vdash S\). This im­me­di­ately im­plies that if \(PA\) is con­sis­tent, the sen­tences \(PA\vdash Prv(S)\implies S\) are not prov­able when \(S\) is false, even though ac­cord­ing to our in­tu­itive un­der­stand­ing of the stan­dard model ev­ery sen­tence of this form must be true.

Thus, \(PA\) is in­com­plete, and fails to prove a par­tic­u­lar set of sen­tences that would in­crease mas­sively our con­fi­dence in it.

No­tice that Gödel’s sec­ond in­com­plete­ness the­o­rem fol­lows im­me­di­ately from Löb’s the­o­rem, as if \(PA\) is con­sis­tent, then by Löb’s \(PA\nvdash Prv(0= 1)\implies 0= 1\), which by the propo­si­tional calcu­lus im­plies \(PA\nvdash \neg Prv(0= 1)\).

It is worth re­mark­ing that Löb’s the­o­rem does not only ap­ply to the stan­dard prov­abil­ity pred­i­cate, but to ev­ery pred­i­cate satis­fy­ing the Hilbert-Ber­nais deriv­abil­ity con­di­tions.



  • Mathematics

    Math­e­mat­ics is the study of num­bers and other ideal ob­jects that can be de­scribed by ax­ioms.