Until-Like Modalities in Topology

Abstract

The topological semantics of modal logic has been an active area of research ever since its introduction in the 1940s, with attention shifting in recent years from standard unimodal logic to more expressive frameworks. This thesis investigates two binary modalities, both of which mimic the Until modality from temporal logic. One is a path-reachability modality γ that has recently been studied in Bezhanishvili et al. (2024) in polyhedral semantics; we investigate its topological counterpart. Focusing on the language combining γ with the classical Cantor derivative modality and the universal modality, we exhibit an axiomatic system sound and complete both for the class of T1 topologies and for the class of all metric spaces, and establish its EXPTIME-completeness. We also axiomatize the logic of all topological spaces in a weaker language obtained by substituting the closure modality for the Cantor derivative. To prove our results, we introduce an equivalent neighborhood-like semantics allowing for the finite model property, and then encode it in a variant of propositional dynamic logic. The second topological modality we address is “until-a-boundary,” proposed by Aiello (2002). We point out that it can express several properties of topologies, notably regularity and zero-dimensionality. We also establish EXPTIME-completeness, though only for the logic of Alexandroff spaces.