Löb's theorem

Remarks

Proof idea: by the diagonal lemma there is $\psi$ with $T \vdash \psi \leftrightarrow (\mathrm{Prov}_T(\ulcorner \psi \urcorner) \to \varphi)$. The derivability conditions of $\mathrm{Prov}_T$, which $T$ proves, give $T \vdash \mathrm{Prov}_T(\ulcorner \psi \urcorner) \to \mathrm{Prov}_T(\ulcorner \varphi \urcorner)$. With the hypothesis this yields $T \vdash \mathrm{Prov}_T(\ulcorner \psi \urcorner) \to \varphi$, hence $T \vdash \psi$, hence $T \vdash \mathrm{Prov}_T(\ulcorner \psi \urcorner)$, and finally $T \vdash \varphi$.

Example: take $\varphi$ to be $0 = S0$. If $T$ proved $\mathrm{Con}(T)$, that is, $\neg \mathrm{Prov}_T(\ulcorner 0 = S0 \urcorner)$, then $T$ would prove $\mathrm{Prov}_T(\ulcorner 0 = S0 \urcorner) \to 0 = S0$, and so $T \vdash 0 = S0$. So a consistent $T$ does not prove its own consistency, which is the second of Gödel's incompleteness theorems. Another consequence: the sentence that says "I am provable" is provable, which answers a question of Henkin.

Going deeper

For a student

Löb's theorem generalizes the second incompleteness theorem, as the example shows. Its formalized version, $\square(\square p \to p) \to \square p$, is the characteristic axiom of the modal provability logic $\mathsf{GL}$, read with $\square$ as "it is provable in $T$ that".