A topological model for provability logic

Gödel’s incompleteness theorem illustrated the need to distinguish between what is true and what is provable. There are true statements that cannot be proven. Let □p denote the assertion that p is provable in Peano arithmetic. The logic with this interpretation for the □ operator is the Gödel-Löb logic, also called provability logic. This is a normal modal logic with the additional axiom □(□p → p) → □p, known as Löb’s axiom. A couple days ago I wrote about topological models for modal logic. Is there a topological model for Gödel-Löb logic? There is, but it’s not quite the same construction as in the previous post. A topological model of Gödel-Löb logic associates p with a set P and ◇p with the derived set of P rather than its closure. The difference between the closure of P and the derived set of P is subtle, but important to this discussion. The closure of a set P is the union of P and all of its limit points. The derived set of P is the set of limit points of P. The distinction is…