If Gödel’s First Incompleteness Theorem showed that formal systems have blind spots, his Second Incompleteness Theorem delivered the fatal blow to David Hilbert’s dream of securing mathematical foundations. Gödel proved that no consistent formal system can ever prove its own consistency. Later generalized by Martin Löb in 1955 into a profound theorem about provability reflection, Gödel’s Second Theorem established that the sanity of reason can only ever be certified from without.
1. The Formalized Consistency Statement $text{Con}(T)$
A formal system $T$ is consistent if it cannot derive a contradiction ($T notvdash bot$, or $T notvdash 0 = 1$). In the arithmetized language of syntax, the formula $bot$ has a specific Gödel number $ulcorner 0 = 1 urcorner$. Therefore, the proposition “Theory $T$ is consistent” can be formalized inside arithmetic as:
[
text{Con}(T) equiv neg text{Prov}_T(ulcorner 0 = 1 urcorner)
]
$text{Con}(T)$ is a $Pi_1$-sentence asserting: “There does not exist any integer $x$ that encodes a valid derivation of $0 = 1$ in $T$.”
2. The Hilbert-Bernays-Löb Derivability Conditions
To prove that $T$ cannot prove $text{Con}(T)$, David Hilbert, Paul Bernays (1939), and Martin Löb (1955) isolated three necessary and sufficient conditions that a provability predicate $Box phi equiv text{Prov}_T(ulcorner phi urcorner)$ must satisfy:
The HBL Derivability Conditions
- D1 (Necessitation): If $T vdash phi$, then $T vdash Box phi$.
- D2 (Distribution): $T vdash Box(phi to psi) to (Box phi to Box psi)$.
- D3 (Internal Provability): $T vdash Box phi to Box Box phi$.
Condition D1 states that if $phi$ is provable, $T$ can recognize that proof. D2 shows that Modus Ponens can be internalized. D3 states that $T$ can formally verify its own proof-verification algorithm.
3. Gödel’s Second Incompleteness Theorem
Gödel’s Second Theorem
Let $T$ be a consistent formal theory capable of elementary arithmetic and satisfying the HBL derivability conditions. Then:
[
T notvdash text{Con}(T)
]
The theory $T$ cannot prove its own consistency.
Proof:
- In the proof of the First Incompleteness Theorem, we showed metamathematically: $text{“If } T text{ is consistent, then } G text{ is not provable.”}$ That is, $text{Con}(T) to G$.
- Because this deduction uses only elementary constructive arithmetic, the entire proof can be formalized inside $T$ itself!
- Using conditions D1, D2, and D3, one rigorously demonstrates:
[
T vdash text{Con}(T) to G
] - Now, suppose for contradiction that $T vdash text{Con}(T)$.
- By Modus Ponens on the implication above, it follows immediately that $T vdash G$.
- However, Gödel’s First Incompleteness Theorem established that if $T$ is consistent, $T notvdash G$!
- Contradiction! Therefore, $T notvdash text{Con}(T)$. $blacksquare$
4. Löb’s Theorem & The Paradox of Modesty
In 1955, Martin Löb investigated Leon Henkin’s question: what about a sentence that asserts its own provability ($psi leftrightarrow Box psi$)? Is it true or false? Löb discovered a astonishing general theorem:
Löb’s Theorem
For any sentence $phi$:
[
T vdash Box phi to phi iff T vdash phi
]
Löb’s Theorem asserts something counter-intuitive: if a theory $T$ can prove that “If $phi$ is provable, then $phi$ is true” (the reflection principle for $phi$), then $T$ must already be able to prove $phi$ directly!
Gödel’s Second Incompleteness Theorem is simply the special case where $phi = bot$. Since $T notvdash bot$, Löb’s theorem immediately implies $T notvdash Box bot to bot$, which is algebraically identical to $T notvdash neg Box bot$ (i.e., $T notvdash text{Con}(T)$).
5. Modal Provability Logic $mathbf{GL}$
The behavior of $Box$ under the HBL conditions corresponds exactly to the Gödel-Löb modal logic $mathbf{GL}$. In $mathbf{GL}$, the box operator $Box$ represents formal provability rather than metaphysical necessity. The defining axiom is:
[
Box(Box P to P) to Box P
]
By Robert Solovay’s Arithmetical Completeness Theorem (1976), $mathbf{GL}$ is complete with respect to Peano Arithmetic: a modal formula is provable in $mathbf{GL}$ if and only if every arithmetical interpretation of $Box$ is provable in $text{PA}$. Modal logic thus completely maps the topological frontier of mathematical self-knowledge.
