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