Logical Methods in Computer Science (Dec 2023)
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\colon X\to X$. We introduce the logics $\bf{wK4C}$, $\bf{K4C}$ and $\bf{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 $\bf{wK4C}$ is the $d$-logic of all dynamic topological systems, $\bf{K4C}$ is the $d$-logic of all $T_D$ dynamic topological systems, and $\bf{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 $\bf{wK4H}$, $\bf{K4H}$ and $\bf{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 $\bf{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.
Keywords