Gödel II and Löb's theorem

https://arbital.com/p/5hs

by Jaime Sevilla Molina Jul 21 2016 updated Jul 25 2016

[summary: [ Gödel's second incompleteness theorem] and [ Löb's theorem] are equivalent to each other. ]

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.