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\).