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

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 that not every point of P is necessarily a limit point of P. A point x is a limit point of P if every open set containing x contains a point of P in addition to x itself.

A topological space X that models Gödel-Löb logic must be scattered, meaning that every open set must contain an isolated point, a point with no limit points. For example, consider

with the topology inherited from the ordinary topology on the real line. Then every point except 0 is isolated, and every open set contains isolated points.

A statement in Gödel-Löb logic is true if its topological interpretation holds for all scattered spaces.