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

Children:

Parents:

• Mathematics

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

• Some­thing I learnt from Mietek Bak is that Löb’s The­o­rem is kind of more sub­tle than this. In prov­abil­ity the­ory, it’s fine to have a “box” op­er­a­tor that we in­for­mally read as “is prov­able”; but what Löb’s the­o­rem tells us that we can’t sim­ply in­ter­pret it liter­ally as “is prov­able” with­out difficul­ties. One should define the “prov­abil­ity” pred­i­cate for­mally, to avoid get­ting con­fused (or one should spec­ify that it is sim­ply a for­mal sym­bol to which we have not as­signed any se­man­tic mean­ing, al­though that is some­what against the point of the an­gle taken by the par­ent ar­ti­cle); for ex­am­ple, the prov­abil­ity pred­i­cate could be defined by a cer­tain first-or­der for­mula which un­packs a Gödel num­ber, checks it’s en­cod­ing a proof and ver­ifies each step of the en­coded proof.

• Yeah, that is the for­mal defi­ni­tion of the stan­dard prov­abil­ity pred­i­cate. I’ll add the page ex­plain­ing that soon enough.