Provability logic seeks to efficiently describe, by suitable axioms and rules of inference, what a reasonable theory can prove about its own provability predicate. Here “reasonable” means that the theory can prove basic facts about the natural numbers; Peano arithmetic is more than enough.

The notation used in provability logic (meaning in the particular provability logic that I’ll concentrate on) is the same as in most modal logics, namely ordinary propositional logic plus a modal operator, written as a box. But the box operator has the unusual interpretation “it is provable that”. It turns out that this provability logic can be axiomatized by adding to ordinary propositional logic just one axiom (schema) and one inference rule. The rule is very simple, but the axiom expresses Löb’s theorem, a far from obvious fact about provability.

I’ll begin by explaining Löb’s theorem. Then I’ll discuss the axiomatic system of provability logic and a few proofs in that system. Next, I’ll describe the Kripke models of provability logic. Finally, I’ll discuss two completeness theorems for this logic, one saying that Kripke models provide a complete semantics, and the other saying that provability logic exactly captures what a reasonable theory can prove about its own provability.