Provability Logic
Provability logic (also called Gödel-Löb logic, GL) is a modal logic where is interpreted as formal provability in Peano Arithmetic. It provides a modal-logical analysis of the incompleteness theorems and self-referential reasoning.
The Logic GL
The logic is the normal modal logic axiomatized by plus the Löb axiom: GL is sound and complete for the class of finite, transitive, irreflexive frames (equivalently, transitive well-founded frames).
An arithmetical interpretation maps propositional variables to arithmetic sentences and to the provability predicate . A modal formula is arithmetically valid if for every arithmetical interpretation , PA proves .
Solovay's Completeness Theorem
Solovay's Arithmetical Completeness Theorem (1976): A modal formula is a theorem of GL if and only if is arithmetically valid. This means GL captures exactly the modal-logical principles of provability in PA. For example, (consistency) is not a theorem of GL, corresponding to the second incompleteness theorem.
Every modal formula has a fixed point in GL: for any formula where occurs only under , there is a formula (not containing ) such that . Moreover, this fixed point is unique modulo GL-provable equivalence. This is the modal counterpart of the diagonal lemma.
Interpretability Logic
Interpretability logic extends provability logic with a binary modality meaning "theory interprets ." The logic ILM (Interpretability Logic with the Montagna principle) extends GL and captures the interpretability relation between extensions of PA.
In GL, the second incompleteness theorem becomes: . That is, GL cannot prove that "consistency" is provable, perfectly mirroring the arithmetic situation. Löb's theorem subsumes both incompleteness theorems: setting , we get , so if PA proved its own consistency, it would prove everything.