一句话:为动态拓扑系统中的 Cantor 导数模态逻辑建立有限模型性质与完备性证明方法。
Cantor 导数算子上的模态逻辑称为 d-逻辑,但此前未在动力系统 (X,f) 框架下研究。本文引入 wK4C、K4C 和 GLC 三个逻辑,证明它们具有有限 Kripke 模型性质,并分别相对于所有动态拓扑系统、T_D 动态拓扑系统以及基于 scattered 空间的动态拓扑系统在 d-语义下可靠且完备。作者还给出 f 为同胚时的一般结果,得到 wK4H、K4H 和 GLH 的可靠完备性。主要贡献是奠定动态拓扑 d-逻辑的有限模型性质与完备性的一般证明方法;GLC 的结果是迈向三模态拓扑-时序语言有限公理化完备性的第一步。
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.