The Second Incompleteness Theorem

Introduction

While Gödel's First Incompleteness Theorem showed that sufficiently powerful formal systems contain undecidable statements, the Second Incompleteness Theorem delivers an even more devastating blow to Hilbert's program. It demonstrates that no consistent formal system can prove its own consistency—a result that shattered hopes for a complete foundation of mathematics.

Statement of the Second Incompleteness Theorem

Theorem (Gödel's Second Incompleteness Theorem): If a formal system S is consistent and contains basic arithmetic (specifically, if S extends Peano Arithmetic), then S cannot prove its own consistency. More formally:

If S ⊢ Con(S), then S is inconsistent.

Where Con(S) is a formula expressing "S is consistent" within the language of S itself.

The Consistency Formula

The key insight is that consistency can be expressed arithmetically. A system S is consistent if and only if there is no formula φ such that both S ⊢ φ and S ⊢ ¬φ. We can encode this as:

Con(S) ≡ ¬∃x(Proof_S(x, ⌜0=1⌜))

This formula states "there is no proof in S of the contradiction 0=1." Since 0=1 represents an arbitrary contradiction, proving this formula would establish S's consistency.

Proof Sketch

The proof elegantly combines the First Incompleteness Theorem with provability logic:

1. From the First Theorem: We know there exists a true but unprovable sentence G in S, where G states "G is not provable in S."

2. Key Insight: If S could prove its own consistency Con(S), then S could prove G.

3. The Contradiction: But we know from the First Theorem that if S is consistent, then S cannot prove G.

4. Conclusion: Therefore, if S is consistent, it cannot prove Con(S).

Detailed Argument

The crucial step is showing that Con(S) → G is provable within S itself. Here's why:

• If S is consistent, then S cannot prove both G and ¬G
• Since G says "G is not provable," if S proves G, then what G says is false
• This would mean G is provable but false, making S inconsistent
• Therefore, if S is consistent, G must be true (hence unprovable)

This reasoning can be formalized within S, giving us S ⊢ (Con(S) → G).

Provability Logic

Provability logic provides the formal framework for reasoning about what a system can prove about its own proofs. Key principles include:

Löb's Theorem

If S ⊢ (Prov_S(⌜φ⌜) → φ), then S ⊢ φ.

This theorem is crucial for understanding self-reference in formal systems and provides another route to the Second Incompleteness Theorem.

The Provability Conditions

For any sound provability predicate Prov_S(x):

1. If S ⊢ φ, then S ⊢ Prov_S(⌜φ⌜)
2. S ⊢ (Prov_S(⌜φ⌜) → Prov_S(⌜Prov_S(⌜φ⌜)⌜))
3. S ⊢ (Prov_S(⌜φ → ψ⌜) ∧ Prov_S(⌜φ⌜) → Prov_S(⌜ψ⌜))

These conditions ensure that the provability predicate behaves correctly for self-referential reasoning.

Philosophical Implications

The Second Incompleteness Theorem has profound implications:

• Hilbert's Program Failed: The dream of proving mathematics consistent from within itself is impossible
• Meta-mathematical Perspective Required: To prove consistency, we must step outside the system
• Relative Consistency: We can only prove consistency relative to stronger systems

Modern Applications

The theorem's techniques appear throughout:

• Computer Science: Verification of program correctness
• Proof Theory: Understanding the strength of different logical systems
• Philosophy: Questions about mathematical truth and knowledge

The Second Incompleteness Theorem stands as one of the most elegant and devastating results in mathematical logic, forever changing our understanding of formal systems and mathematical truth.