Gödel II and Löb's theorem

The ab­stract form of Gödel’s sec­ond in­com­plete­ness the­o­rem states that if \(P\) is a prov­abil­ity pred­i­cate in a con­sis­tent, ax­iom­a­ti­z­able the­ory \(T\) then \(T\not\vdash \neg P(\ulcorner S\urcorner)\) for a dis­prov­able \(S\).

On the other hand, Löb’s the­o­rem says that in the same con­di­tions and for ev­ery sen­tence \(X\), if \(T\vdash P(\ulcorner X\urcorner)\rightarrow X\), then \(T\vdash X\).

It is easy to see how GII fol­lows from Löb’s. Just take \(X\) to be \(\bot\), and since \(T\vdash \neg \bot\) (by defi­ni­tion of \(\bot\)), Löb’s the­o­rem tells that if \(T\vdash \neg P(\ulcorner \bot\urcorner)\) then \(T\vdash \bot\). Since we as­sumed \(T\) to be con­sis­tent, then the con­se­quent is false, so we con­clude that \(T\neg\vdash \neg P(\ulcorner \bot\urcorner)\).

The rest of this ar­ti­cle ex­poses how to de­duce Löb’s the­o­rem from GII.

Sup­pose that \(T\vdash P(\ulcorner X\urcorner)\rightarrow X\).

Then \(T\vdash \neg X \rightarrow \neg P(\ulcorner X\urcorner)\).

Which means that \(T + \neg X\vdash \neg P(\ulcorner X\urcorner)\).

From Gödel’s sec­ond in­com­plete­ness the­o­rem, that means that \(T+\neg X\) is in­con­sis­tent, since it proves \(\neg P(\ulcorner X\urcorner)\) for a dis­prov­able \(X\).

Since \(T\) was con­sis­tent be­fore we in­tro­duced \(\neg X\) as an ax­iom, then that means that \(X\) is ac­tu­ally a con­se­quence of \(T\). By com­plete­ness, that means that we should be able to prove \(X\) from \(T\)’s ax­ioms, so \(T\vdash X\) and the proof is done.