A topological model for provability logic

Godel'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 thatp is provable in Peano arithmetic. The logic with this interpretation for the operator is the Godel-Lob logic, also called provability logic. This is a normal modal logic with the additional axiom

(pp) p,

known as Lob's axiom.

A couple days ago I wrote about topological models for modal logic. Is there a topological model for Godel-Lob logic? There is, but it's not quite the same construction as in the previous post.

A topological model of Godel-Lob logic associatesp with a set P and p with thederived set ofP rather than its closure.

The difference between the closure ofP 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 Godel-Lob logic must bescattered, meaning that every open set must contain an isolated point, a point with no limit points. For example, consider

X = {0} {1, , , 1/4, ...}

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 Godel-Lob logic is true if its topological interpretation holds forall scattered spaces.

The post A topological model for provability logic first appeared on John D. Cook.