Gödel II and Löb's theorem

The abstract form of Gödel’s second incompleteness theorem states that if \(P\) is a provability predicate in a consistent, axiomatizable theory \(T\) then \(T\not\vdash \neg P(\ulcorner S\urcorner)\) for a disprovable \(S\).

On the other hand, Löb’s theorem says that in the same conditions and for every sentence \(X\), if \(T\vdash P(\ulcorner X\urcorner)\rightarrow X\), then \(T\vdash X\).

It is easy to see how GII follows from Löb’s. Just take \(X\) to be \(\bot\), and since \(T\vdash \neg \bot\) (by definition of \(\bot\)), Löb’s theorem tells that if \(T\vdash \neg P(\ulcorner \bot\urcorner)\) then \(T\vdash \bot\). Since we assumed \(T\) to be consistent, then the consequent is false, so we conclude that \(T\neg\vdash \neg P(\ulcorner \bot\urcorner)\).

The rest of this article exposes how to deduce Löb’s theorem from GII.

Suppose 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 second incompleteness theorem, that means that \(T+\neg X\) is inconsistent, since it proves \(\neg P(\ulcorner X\urcorner)\) for a disprovable \(X\).

Since \(T\) was consistent before we introduced \(\neg X\) as an axiom, then that means that \(X\) is actually a consequence of \(T\). By completeness, that means that we should be able to prove \(X\) from \(T\)’s axioms, so \(T\vdash X\) and the proof is done.