Provability Logic

Origin. Gödel noted the connection between modal logic and provability (1933). Robert Solovay proved arithmetic completeness of GL (1976): the modal logic of provability in Peano Arithmetic. George Boolos developed the field extensively (The Logic of Provability, 1993). Bridges modal logic, proof theory, and foundations of mathematics.

Models. Provability as a modality. □φ means "φ is provable in PA." The box isn't necessity but formal derivability. Gödel's incompleteness theorems become modal facts: □⊥ → ⊥ fails (PA doesn't prove its own consistency unless inconsistent). The logic GL captures exactly what PA can prove about its own provability predicate.

Formalism.

The logic GL (Gödel-Löb): All propositional tautologies, plus:

• K: □(φ → ψ) → (□φ → □ψ)
• Löb's axiom: □(□φ → φ) → □φ
• Necessitation: if ⊢ φ then ⊢ □φ

Key theorems:

• □φ → □□φ (provability is provable)
• ¬□⊥ not provable (can't prove consistency — Gödel)
• □(□φ → φ) → □φ (Löb's theorem)

What GL lacks:

• □φ → φ (T axiom) — provability doesn't imply truth
• φ → □φ — truth doesn't imply provability

Arithmetic interpretation: Let PA be Peano Arithmetic with Gödel numbering. Prov(n) = "n is the Gödel number of a provable sentence" □φ interpreted as Prov(⌜φ⌝)

Solovay's completeness: GL ⊢ φ iff for all arithmetic interpretations , PA ⊢ φ

Fixed points: For any modal formula φ(p) with p only under □, there exists ψ with no p such that GL ⊢ ψ ↔ φ(ψ). Example: Gödel sentence is fixed point of ¬□p.

Kripke semantics: GL is complete for finite, transitive, irreflexive frames (converse well-founded). Worlds = "stages of knowledge," accessibility = "extension."

Symbols.

Metatheory. GL is decidable (PSPACE-complete). Arithmetic completeness (Solovay): GL = provability logic of PA. The second incompleteness theorem: GL ⊬ ¬□⊥. Fixed point theorem: every formula has a fixed point. GLS (GL + □φ → φ) = logic of true provability (what's both provable and true). Interpretability logic extends GL to relative interpretability.

Applies to. Foundations of mathematics. Self-referential reasoning. Formalizing Gödel's theorems. Verification (what can a system prove about itself). Epistemic logic of idealized reasoners. Ordinal analysis.

Limitations. Only captures what PA proves about provability — not about truth. The Kripke semantics is non-standard (irreflexive). □φ → φ fails, making it different from knowledge/necessity. Arithmetic completeness is specific to PA-like systems. The modal language is limited; quantified provability logic is much harder.

© 2026 Lingenic LLC