Löb's theorem and computer programs

The close re­la­tion­ship be­tween logic and com­putabil­ity al­lows us to frame Löb’s the­o­rem in terms of a com­puter pro­gram which is sys­tem­at­i­cally look­ing for proofs of math­e­mat­i­cal state­ments, ProofSeeker(X).

ProofSeeker can be some­thing like this:

        if Prv(X,n): re­turn True
        else n = n+1

Where Prv(X,n) is true if \(n\) en­codes a proof of \(X\)noteSee stan­dard prov­abil­ity pred­i­cate for more info on how to talk about prov­ablity.

Now we form a spe­cial sen­tence called a re­flec­tion prin­ci­ple, of the form \(L(X)\)= “If ProofSeeker(X) halts, then X is true”. (This re­quires a quine to con­struct.)

Reflec­tion prin­ci­ples are in­tu­itively true, since ProofSeeker clearly halts iff it finds a proof of \(X\), and if there is a proof of \(X\), then \(X\) must be true if we have cho­sen an ap­pro­pri­ate log­i­cal sys­tem to search for proofs. For ex­am­ple, let’s say that ProofSeeker is look­ing for proofs within Peano Arith­metic.

The ques­tion now be­comes, what hap­pens when we call ProofSeeker on \(L(X)\)? Is \(PA\) ca­pa­ble of prov­ing that the re­flec­tion prin­ci­ple for any given \(X\) is true, and there­fore ProofSeeker will even­tu­ally halt? Or will it run for­ever?

Sev­eral pos­si­bil­ities ap­pear:

  1. If \(PA\vdash X\), then cer­tainly \(PA\vdash L(X)\), since if the con­se­quent of \(L(X)\) is prov­able, then the whole sen­tence is prov­able.

  2. If \(PA\vdash \neg X\), then we can­not as­sert that \(PA\vdash L(X)\), for that would im­ply as­sert­ing that \(PA\vdash\)“There is no proof of X”. This is tan­ta­mount to \(PA\) as­sert­ing the con­sis­tency of \(PA\), which is for­bid­den by Gödel’s sec­ond in­com­plete­ness the­o­rem.

  3. If \(X\) is un­de­cid­able in \(PA\), then if it were the case that \(PA\vdash L(X)\) it would be in­con­sis­tent that \(PA\vdash \neg X\) for the same rea­son as when \(X\) is dis­prov­able, and thus \(PA\vdash X\), con­tra­dict­ing that it was un­de­cid­able.

Löb’s the­o­rem is the as­ser­tion that \(PA\) proves the re­flec­tion prin­ci­ple for \(X\) only if \(PA\) proves \(X\).

Or con­versely, Löb’s the­o­rem states that if \(PA\not\vdash X\) then \(PA\not\vdash \square_{PA} X \rightarrow X\).

It can be proved in \(PA\) and stronger sys­tems. It has a very strong link with Gödel’s sec­ond in­com­plete­ness the­o­rem, and in fact they both are equiv­a­lent.