# Proof of Löb's theorem

The in­tu­ition be­hind the proof of Löb’s the­o­rem in­vokes the for­mal­iza­tion of the fol­low­ing ar­gu­ment:

Let $$S$$ stand for the sen­tence “If $$S$$ is prov­able, then I am Santa Claus”.

As it is stan­dard, when try­ing to prove a If…then the­o­rem we can start by sup­pos­ing the an­tecedent and check­ing that the con­se­quent fol­lows. But if $$S$$ is prov­able, then we can chain its proof to an ap­pli­ca­tion of modus po­nens of $$S$$ to it­self in or­der to get a proof of the con­se­quent “I am Santa Claus”. If we sup­pose that show­ing the ex­is­tence of a proof of a sen­tence im­plies that the sen­tence is true, then “I am Santa Claus” is true.

Thus we have sup­posed that $$S$$ is prov­ably true then it fol­lows that “I am Santa Claus”, which is a proof of what $$S$$ states! There­fore, $$S$$ is prov­ably true, and we can ap­ply the same rea­son­ing again (this time with­out sup­pos­ing a coun­ter­fac­tual) to get that it is true that “I am Santa Claus”.

Holy Gödel! Have we bro­ken logic? If this ar­gu­ment worked, then we could prove any non­sen­si­cal thing we wanted. So where does it fail?

One sus­pi­cious point is our im­plicit as­sump­tion that $$S$$ can be con­structed in the first place as a first or­der sen­tence. But we know that there ex­ists a prov­abil­ity pred­i­cate en­cod­ing the mean­ing we need, and then we can ap­ply the di­ag­o­nal lemma to the for­mula $$Prv(x)\implies$$ “I am Santa Claus” to get our de­sired $$S$$.

(We will ig­nore the fact that ex­press­ing “I am Santa Claus” in the lan­guage of first or­der logic is rather difficult, since we could eas­ily re­place it with some­thing sim­ple like $$0=1$$.)

It turns out that the culprit of this para­dox is the ap­par­ently in­no­cent sup­po­si­tion that when “I am Santa Claus” is prov­able, then it is true.

How can this be false?, you may ask. Well, the stan­dard prov­abil­ity pred­i­cate $$Prv$$ is some­thing of the form $$\exists y Proof(x,y)$$, where $$Proof(x,y)$$ is true iff $$y$$ en­codes a valid proof of $$x$$. But $$y$$ might be a non­stan­dard num­ber en­cod­ing a non­stan­dard proof of in­finitely many steps. If the only proofs of $$x$$ are non­stan­dard then cer­tainly you will never be able to prove $$x$$ from the ax­ioms of the sys­tem us­ing stan­dard meth­ods.

We can restate this re­sult as Löb’s the­o­rem: If $$Prv(A)\implies A$$ is prov­able, then $$A$$ is prov­able.

Now we go for the for­mal proof.

Let $$T$$ be an ax­iom­a­ti­z­able ex­ten­sion of min­i­mal ar­ith­metic, and $$P$$ a one-place pred­i­cate satis­fy­ing the Ber­nais-Hilbert deriv­abil­ity con­di­tions, which are:

1. If $$T\vdash A$$, then $$T\vdash P(A)$$.

2. $$T\vdash P(A\implies B) \implies (P(A)\implies P(B))$$

3. $$T\vdash P(A)\implies P(P(A))$$.

For ex­am­ple, $$PA$$ and the stan­dard prov­abil­ity pred­i­cate satisfy those con­di­tions.

Let us sup­pose that $$A$$ is such that $$T\vdash P(A)\implies A$$.

As $$T$$ ex­tends min­i­mal ar­ith­metic, the di­ag­o­nal lemma is ap­pli­ca­ble, and thus there ex­ists $$S$$ such that $$T\vdash S \iff (P(S)\implies A)$$.

By con­di­tion 1, $$T\vdash P(S \implies (P(S)\implies A))$$.

By con­di­tion 2, $$T\vdash P(S) \implies P(P(S) \implies A)$$.

Also by con­di­tion 2, $$T\vdash P(P(S) \implies A) \implies (P(P(S)) \implies P(A))$$.

Com­bin­ing these, $$T\vdash P(S) \implies (P(P(S)) \implies P(A))$$.

By con­di­tion 3, $$T\vdash P(S)\implies P(P(S))$$ and thus $$T\vdash P(S)\implies P(A)$$.

By our ini­tial as­sump­tion, this means that $$T\vdash P(S)\implies A$$.

But by the con­struc­tion of $$S$$, then $$T\vdash S$$!

By con­di­tion 1 again, then $$T\vdash P(S)$$, and since we already had shown that $$T\vdash P(S)\implies A$$, we have that $$T\vdash A$$, which com­pletes the proof.

We re­mark that $$P$$ can be any pred­i­cate satis­fy­ing the con­di­tions, such as the verum pred­i­cate $$x=x$$.

Parents:

• This is one of two ways I know of prov­ing Löb’s the­o­rem, and I find them both illu­mi­nat­ing. (The other is to de­rive it from Gödel’s Se­cond In­com­plete­ness The­o­rem.)