Creative Commons Attribution 4.0 International license
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 → X. We introduce the logics wK4C, K4C and 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 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 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 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.
@InProceedings{fernandezduque_et_al:LIPIcs.CSL.2022.19,
author = {Fern\'{a}ndez-Duque, David and Montacute, Yo\`{a}v},
title = {{Dynamic Cantor Derivative Logic}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {19:1--19:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.19},
URN = {urn:nbn:de:0030-drops-157397},
doi = {10.4230/LIPIcs.CSL.2022.19},
annote = {Keywords: dynamic topological logic, Cantor derivative, temporal logic, modal logic}
}