Provability logic

Summary

Provability logic is the modal logic in which $\square\varphi$ is read as "$\varphi$ is provable" in a formal theory such as Peano arithmetic. Its main system $\mathrm{GL}$ is the normal modal logic given by Löb's axiom $\square(\square p \to p) \to \square p$. By Solovay's theorem, $\mathrm{GL}$ proves exactly the modal laws of provability in Peano arithmetic, so questions about provability become finite combinatorics of Kripke frames.