Fixed Point Logics on Hemimetric Spaces
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F23%3A00574237" target="_blank" >RIV/67985807:_____/23:00574237 - isvavai.cz</a>
Výsledek na webu
<a href="https://dx.doi.org/10.1109/LICS56636.2023.10175784" target="_blank" >https://dx.doi.org/10.1109/LICS56636.2023.10175784</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1109/LICS56636.2023.10175784" target="_blank" >10.1109/LICS56636.2023.10175784</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Fixed Point Logics on Hemimetric Spaces
Popis výsledku v původním jazyce
The μ-calculus can be interpreted over metric spaces and is known to enjoy, among other celebrated properties, variants of the McKinsey-Tarski completeness theorem and of Dawar and Otto's modal characterization theorem. In its topological form, this theorem states that every topological fixed point may be defined in terms of the tangled derivative, a polyadic generalization of Cantor's perfect core. However, these results fail when spaces not satisfying basic separation axioms are considered, in which case the base modal logic is not the well-known K4, but the weaker wK4.In this paper we show how these shortcomings may be overcome. First, we consider semantics over the wider class of hemimetric spaces, and obtain metric completeness results for wK4 and related logics. In this setting, the Dawar-Otto theorem still fails, but we argue that this is due to the tangled derivative not being suitably defined for general application in arbitrary topological spaces. We thus introduce the hybrid tangle, which coincides with the tangled derivative over metric spaces but is better behaved in general. We show that only the hybrid tangle suffices to define simulability of finite structures, a key 'test case' for an expressively complete fragment of the μ-calculus.
Název v anglickém jazyce
Fixed Point Logics on Hemimetric Spaces
Popis výsledku anglicky
The μ-calculus can be interpreted over metric spaces and is known to enjoy, among other celebrated properties, variants of the McKinsey-Tarski completeness theorem and of Dawar and Otto's modal characterization theorem. In its topological form, this theorem states that every topological fixed point may be defined in terms of the tangled derivative, a polyadic generalization of Cantor's perfect core. However, these results fail when spaces not satisfying basic separation axioms are considered, in which case the base modal logic is not the well-known K4, but the weaker wK4.In this paper we show how these shortcomings may be overcome. First, we consider semantics over the wider class of hemimetric spaces, and obtain metric completeness results for wK4 and related logics. In this setting, the Dawar-Otto theorem still fails, but we argue that this is due to the tangled derivative not being suitably defined for general application in arbitrary topological spaces. We thus introduce the hybrid tangle, which coincides with the tangled derivative over metric spaces but is better behaved in general. We show that only the hybrid tangle suffices to define simulability of finite structures, a key 'test case' for an expressively complete fragment of the μ-calculus.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10101 - Pure mathematics
Návaznosti výsledku
Projekt
<a href="/cs/project/GA22-01137S" target="_blank" >GA22-01137S: Metamatematika substrukturálních modálních logik</a><br>
Návaznosti
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Ostatní
Rok uplatnění
2023
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ů
Údaje specifické pro druh výsledku
Název statě ve sborníku
38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) Proceedings
ISBN
979-8-3503-3588-0
ISSN
—
e-ISSN
—
Počet stran výsledku
13
Strana od-do
190687
Název nakladatele
IEEE
Místo vydání
New York
Místo konání akce
Boston
Datum konání akce
26. 6. 2023
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
001036707700049