Gödel II and Löb's theorem

Discussion5

Written by Jaime Sevilla Molina last updated 21st Jul 2016

Title

Tab title

Tab subtitle

The abstract form of Gödel's second incompleteness theorem states that if

is a provability predicate in a consistent, axiomatizable theory then for a disprovable .

On the other hand, Löb's theorem says that in the same conditions and for every sentence

, if , then .

It is easy to see how GII follows from Löb's. Just take

to be , and since (by definition of ), Löb's theorem tells that if then . Since we assumed to be consistent, then the consequent is false, so we conclude that .

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 for a disprovable .

Since

was consistent before we introduced as an axiom, then that means that is actually a consequence of . By completeness, that means that we should be able to prove from 's axioms, so and the proof is done.

Summaries

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.