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.
翻译:基于康托尔导数算子的模态逻辑拓扑语义催生了导数逻辑,亦称为$d$-逻辑。与基于拓扑闭包算子的逻辑不同,$d$-逻辑此前尚未在动力系统框架下得到研究。动力系统定义为对$(X,f)$,其中$X$为拓扑空间,$f\colon X\to X$为连续函数。本文引入逻辑系统$\bf{wK4C}$、$\bf{K4C}$和$\bf{GLC}$,证明它们均具有有限克里普克模型性质,且相对于该动力设定下的$d$-语义具有可靠性与完全性。具体而言,我们证明$\bf{wK4C}$是所有动态拓扑系统的$d$-逻辑,$\bf{K4C}$是所有$T_D$动态拓扑系统的$d$-逻辑,而$\bf{GLC}$则是基于离散空间的所有动态拓扑系统的$d$-逻辑。此外,我们针对$f$为同胚映射的情形给出一般性结论,由此推导出相应系统$\bf{wK4H}$、$\bf{K4H}$和$\bf{GLH}$的可靠性与完全性。本研究的主要贡献在于建立了一种适用于动态拓扑$d$-逻辑有限模型性质与完全性证明的通用方法。更进一步,关于$\bf{GLC}$的结论为证明三模态时态拓扑语言相对于有限公理化的完全性迈出了第一步——而该公理化在全体空间类中已知是不可能的。