Gödel II and Löb's theorem

Edited by Jaime Sevilla Molina last updated 21st Jul 2016

The abstract form of Gödel's second incompleteness theorem states that if is a provability predicate in a consistent, axiomatizable theory $T$ then $T ⊬ \neg P (┌ S ┐)$ 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 ⊢ P (┌ X ┐) \to X$ , then $T ⊢ X$ .

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

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

Suppose that $T ⊢ P (┌ X ┐) \to X$ .

Then $T ⊢ \neg X \to \neg P (┌ X ┐)$ .

Which means that $T + \neg X ⊢ \neg P (┌ X ┐)$ .

From Gödel's second incompleteness theorem, that means that $T + \neg X$ is inconsistent, since it proves $\neg P (┌ X ┐)$ 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 ⊢ X$ and the proof is done.