Dynamic Cantor Derivative Logic

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F22%3A00557159" target="_blank" >RIV/67985807:_____/22:00557159 - isvavai.cz</a>

Výsledek na webu

<a href="https://drops.dagstuhl.de/opus/volltexte/2022/15739/pdf/LIPIcs-CSL-2022-19.pdf" target="_blank" >https://drops.dagstuhl.de/opus/volltexte/2022/15739/pdf/LIPIcs-CSL-2022-19.pdf</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.CSL.2022.19" target="_blank" >10.4230/LIPIcs.CSL.2022.19</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Dynamic Cantor Derivative Logic

Popis výsledku v původním jazyce

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 TD 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.

Název v anglickém jazyce

Dynamic Cantor Derivative Logic

Popis výsledku anglicky

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 TD 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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10101 - Pure mathematics

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2022

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

30th EACSL Annual Conference on Computer Science Logic

ISBN

—

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

17

Strana od-do

"19:1"-"19:17"

Název nakladatele

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Místo vydání

Dagstuhl

Místo konání akce

Göttingen / Virtual

Datum konání akce

14. 2. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—