Dynamic Cantor Derivative Logic

Abstract

Topological semantics for modal logic based on the Cantor derivative operator gives rise to derivative logics, also referred to as $d$-logics. Unlike logics based on the topological closure operator, $d$-logics have not previously been studied in the framework of dynamical systems, which are pairs $(X,f)$ consisting of a topological space $X$ equipped with a continuous function $f:X\to X$. We introduce the logics $wK4C$, $K4C$ and $\mathbf{GLC}$ and show that they all have the finite Kripke model property and are sound and complete with respect to the $d$-semantics in this dynamical setting. In particular, we prove that $wK4C$ is the $d$-logic of all dynamic topological systems, $K4C$ is the $d$-logic of all $T_D$ dynamic topological systems, and $\mathbf{GLC}$ is the $d$-logic of all dynamic topological systems based on a scattered space. We also prove a general result for the case where $f$ is a homeomorphism, which in particular yields soundness and completeness for the corresponding systems $wK4H$, $K4H$ and $\mathbf{GLH}$. The main contribution of this work is the foundation of a general proof method for finite model property and completeness of dynamic topological $d$-logics. Furthermore, our result for $\mathbf{GLC}$ constitutes the first step towards a proof of completeness for the trimodal topo-temporal language with respect to a finite axiomatisation -- something known to be impossible over the class of all spaces.

arXiv commentExtended version of the paper in Computer Science Logic (CSL) 2022 Proceedings