Proof of Löb's Theorem

Löb's theorem is a remarkable result in provability logic stating that if PA can prove that the provability of a sentence implies the sentence itself, then PA already proves the sentence. It subsumes the second incompleteness theorem.

Statement

Theorem8.3Löb's Theorem

For any arithmetic sentence $\sigma$ : if $\mathrm{PA} \vdash \mathrm{Prov}_{\mathrm{PA}}(\ulcorner \sigma \urcorner) \to \sigma$ , then $\mathrm{PA} \vdash \sigma$ .

Proof

Assume $\mathrm{PA} \vdash \mathrm{Prov}(\ulcorner \sigma \urcorner) \to \sigma$ (we drop the subscript PA for brevity).

Step 1: By the diagonal lemma, let $\theta$ satisfy: $\mathrm{PA} \vdash \theta \leftrightarrow (\mathrm{Prov}(\ulcorner \theta \urcorner) \to \sigma).$

Step 2: From $\theta \leftrightarrow (\mathrm{Prov}(\ulcorner \theta \urcorner) \to \sigma)$ in PA: $\mathrm{PA} \vdash \theta \to (\mathrm{Prov}(\ulcorner \theta \urcorner) \to \sigma).$

Step 3: By the Hilbert-Bernays derivability condition (D2), PA proves: $\mathrm{Prov}(\ulcorner \theta \to (\mathrm{Prov}(\ulcorner \theta \urcorner) \to \sigma) \urcorner).$ By (D2) applied to the implication: $\mathrm{PA} \vdash \mathrm{Prov}(\ulcorner \theta \urcorner) \to \mathrm{Prov}(\ulcorner \mathrm{Prov}(\ulcorner \theta \urcorner) \to \sigma \urcorner).$ By (D2) again: $\mathrm{PA} \vdash \mathrm{Prov}(\ulcorner \theta \urcorner) \to (\mathrm{Prov}(\ulcorner \mathrm{Prov}(\ulcorner \theta \urcorner) \urcorner) \to \mathrm{Prov}(\ulcorner \sigma \urcorner)).$

Step 4: By (D3): $\mathrm{PA} \vdash \mathrm{Prov}(\ulcorner \theta \urcorner) \to \mathrm{Prov}(\ulcorner \mathrm{Prov}(\ulcorner \theta \urcorner) \urcorner)$ .

Combining Steps 3 and 4: $\mathrm{PA} \vdash \mathrm{Prov}(\ulcorner \theta \urcorner) \to \mathrm{Prov}(\ulcorner \sigma \urcorner).$

Step 5: By our assumption: $\mathrm{PA} \vdash \mathrm{Prov}(\ulcorner \sigma \urcorner) \to \sigma$ . Therefore: $\mathrm{PA} \vdash \mathrm{Prov}(\ulcorner \theta \urcorner) \to \sigma$ .

Step 6: By the fixed-point property: $\mathrm{PA} \vdash (\mathrm{Prov}(\ulcorner \theta \urcorner) \to \sigma) \to \theta$ . From Step 5: $\mathrm{PA} \vdash \theta$ .

Step 7: By (D1): $\mathrm{PA} \vdash \mathrm{Prov}(\ulcorner \theta \urcorner)$ . By Step 5: $\mathrm{PA} \vdash \sigma$ . $\square$

■

Deriving the Second Incompleteness Theorem

ExampleSecond Incompleteness from Löb

Set $\sigma = \bot$ (falsehood) in Löb's theorem. The conclusion "PA $\vdash \bot$ " means PA is inconsistent. The hypothesis becomes "PA $\vdash \mathrm{Prov}(\ulcorner \bot \urcorner) \to \bot$ ", which is "PA $\vdash \neg \mathrm{Prov}(\ulcorner \bot \urcorner)$ ", i.e., PA $\vdash \mathrm{Con}(\mathrm{PA})$ . So: if PA $\vdash \mathrm{Con}(\mathrm{PA})$ , then PA is inconsistent. This is the second incompleteness theorem.

RemarkModal Version

In provability logic GL, Löb's theorem is the axiom $\Box(\Box p \to p) \to \Box p$ . Solovay's completeness theorem shows this is the key principle governing provability, and no further modal principles are needed beyond K + Löb.