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.

Symbol	Unicode	Name	Meaning
□	U+25A1	Box / Provability	Provable in PA
◇	U+25C7	Diamond / Consistency	¬□¬; consistent with PA
⊥	U+22A5	Falsum	Contradiction
⊢	U+22A2	Derivability	Provable in the calculus or in PA
⊬	U+22AC	Non-derivability	Not provable
⌜ ⌝	U+231C, U+231D	Corner quotes	Gödel numeral of a formula
↔	U+2194	Biconditional	Fixed-point equivalence
φ, ψ	U+03C6, U+03C8	Phi, psi	Schematic formulas
Prov	—	Provability predicate	Σ₁ formula numerating PA-theorems
GL	—	Gödel–Löb logic	K + Löb; the provability logic of PA
GLS	—	GL plus reflection	GL + (□φ → φ), without necessitation
Löb	—	Löb's axiom	□(□φ → φ) → □φ
PA	—	Peano Arithmetic	The base arithmetical theory
( )*	—	Arithmetical interpretation	Assignment of sentences to atoms

Metatheory. Segerberg (1971) proved GL sound and complete for transitive converse well-founded frames, and it has the finite model property with respect to finite irreflexive transitive trees of depth at most the modal degree of φ, hence is decidable with satisfiability PSPACE-complete. The axiom 4 is redundant: □φ → □□φ is derivable from Löb's axiom in K. GL is Kripke complete but not canonical and not compact — converse well-foundedness is not first-order definable, Löb's axiom is not Sahlqvist, and the canonical frame of GL contains infinite ascending chains. Solovay (1976) proved two arithmetical completeness theorems: GL ⊢ φ iff PA ⊢ φ* for every arithmetical interpretation *, and GLS axiomatizes the formulas true under every interpretation, where GLS is quasi-normal — closed under modus ponens but not under necessitation. The de Jongh–Sambin fixed point theorem gives, for every φ(p) with p only under □, a p-free ψ with GL ⊢ ψ ↔ φ(ψ), and ψ is unique up to GL-provable equivalence. GL enjoys Craig interpolation.

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. Löb's axiom forces irreflexivity, so GL is unsound for every veridical reading: GL + T is inconsistent, since necessitating the T schema and applying Löb's axiom proves □φ, whence T yields every formula, and consequently GL cannot serve as a logic of knowledge, necessity or truth. Solovay's theorem depends on the provability predicate being a standard Σ₁ numeration of a Σ₁-sound theory; Rosser's provability predicate, which is extensionally correct, falsifies Löb's axiom, so GL captures a particular formalization rather than provability as such. GL is Kripke complete but neither canonical nor compact, and no first-order frame condition characterizes it. The propositional restriction is essential: Vardanyan (1986) showed the set of quantified modal formulas provable under all arithmetical interpretations in PA is Π⁰₂-complete, so quantified provability logic has no recursive axiomatization. Beklemishev's polymodal GLP, which stratifies provability by iterated consistency, is Kripke incomplete and requires topological semantics.