paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Dynamic Cantor Derivative Logic

动态 Cantor 导数逻辑
LMCS vol.Volume 19, Issue 42023匹配度 1/10 · 该论文研究动态拓扑系统中的模态逻辑(Cantor 导数逻辑)的有限模型性质与完备性,属于纯逻辑/拓扑语义理论研究,未涉及静态分析、程序分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,与用户研究画像核心方向几乎无关。引用 0 inbox
David Fernández-Duque, Yoàv Montacute
crossref: 2026-09-10

AI 速览

一句话:为动态拓扑系统中的 Cantor 导数模态逻辑建立有限模型性质与完备性证明方法。

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

问题
如何在带连续映射的动态拓扑系统中,为基于 Cantor 导数算子的模态 d-逻辑建立有限模型性质与可靠完备公理化。
方法
引入 wK4C、K4C、GLC 等逻辑,利用有限 Kripke 模型构造和 d-语义证明它们对特定动态拓扑类的可靠完备性,并推广至 f 为同胚的情形。
评估
通过数学证明给出有限模型性质与可靠完备性定理,刻画各逻辑所对应的动态拓扑系统类,并给出同胚变体 wK4H、K4H、GLH 的结果。
原文摘要(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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2167,
  title = {Dynamic Cantor Derivative Logic},
  author = {David Fernández-Duque and Yoàv Montacute},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 19, Issue 4},
  year = {2023},
  doi = {10.46298/lmcs-19(4:26)2023}
}