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

Parents: