Topological interpretations of provability logic

TL;DR

This paper surveys the development of topological semantics for provability logic, highlighting recent advances in polymodal provability logic and its connections to set theory and large cardinals.

Contribution

It provides a comprehensive overview of topological interpretations of provability logic, emphasizing recent results on polymodal logic and unpublished findings.

Findings

Topological semantics offers a complete alternative to Kripke models for GLP.

Polymodal provability logic exhibits complex behavior better captured by topological models.

New unpublished results on topological models of provability logic are presented.

Abstract

Provability logic concerns the study of modality $\Box$ as provability in formal systems such as Peano arithmetic. Natural, albeit quite surprising, topological interpretation of provability logic has been found in the 1970's by Harold Simmons and Leo Esakia. They have observed that the dual $\Diamond$ modality, corresponding to consistency in the context of formal arithmetic, has all the basic properties of the topological derivative operator acting on a scattered space. The topic has become a long-term project for the Georgian school of logic led by Esakia, with occasional contributions from elsewhere. More recently, a new impetus came from the study of polymodal provability logic GLP that was known to be Kripke incomplete and, in general, to have a more complicated behavior than its unimodal counterpart. Topological semantics provided a better alternative to Kripke models in the sense that GLP was shown to be topologically complete. At the same time, new fascinating connections with set theory and large cardinals have emerged. We give a survey of the results on topological semantics of provability logic starting from first contributions by Esakia. However, a special emphasis is put on the recent work on topological models of polymodal provability logic. We also included a few results that have not been published so far, most notably the results of Section 6 (due the second author) and Sections 10, 11 (due to the first author).