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

ProofSeeker(X):
n=1
while(True):
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.

Parents:

• Löb's theorem

Löb’s the­o­rem

• Mathematics

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