David Fernández-Duque: The (poly)topologies of provability logic

Abstract: The Gödel-Löb logic GL is a modal logic which is sound and complete for its arithmetical interpretation, where the modal [] represents Gödel’s provability predicate. It also enjoys both relational and topological semantics, the latter based on Cantor's scattered spaces. There are various completeness results for this interpretation, due to Esakia, Abashidze and Blass.

Meanwhile, Japaridze's polymodal logic GLP is an extension of GL which has one modality [n] for each natural number. These operators also enjoy a natural proof-theoretic interpretation using a notion of n-provability, but in contrast to GL, GLP is incomplete for its relational semantics. Fortunately, it is complete for its topological interpretation, using polytopological spaces with an increasing chain of scattered topologies, as was shown by Beklemishev and Gabelaia. The proof of this is non-constructive and required novel techniques in the study of scattered spaces. Moreover, as the speaker has shown, this result also holds for Beklemishev's transfinite extension of GLP.

In this presentation, we will introduce the logics GL and GLP along with their intended proof-theoretic interpretation. We will discuss their relational and topological semantics, and sketch the main ideas behind the completeness proofs for the latter.