License:
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2022.15
URN: urn:nbn:de:0030-drops-168132
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16813/
Bednarczyk, Bartosz ;
Jaakkola, Reijo
Towards a Model Theory of Ordered Logics: Expressivity and Interpolation
Abstract
We consider the family of guarded and unguarded ordered logics, that constitute a recently rediscovered family of decidable fragments of first-order logic (FO), in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. While the complexities of their satisfiability problems are now well-established, their model theory, however, is poorly understood. Our paper aims to provide some insight into it.
We start by providing suitable notions of bisimulation for ordered logics. We next employ bisimulations to compare the relative expressive power of ordered logics, and to characterise our logics as bisimulation-invariant fragments of FO à la van Benthem.
Afterwards, we study the Craig Interpolation Property (CIP). We refute yet another claim from the infamous work by Purdy, by showing that the fluted and forward fragments do not enjoy CIP. We complement this result by showing that the ordered fragment and the guarded ordered logics enjoy CIP. These positive results rely on novel and quite intricate model constructions, which take full advantage of the "forwardness" of our logics.
BibTeX - Entry
@InProceedings{bednarczyk_et_al:LIPIcs.MFCS.2022.15,
author = {Bednarczyk, Bartosz and Jaakkola, Reijo},
title = {{Towards a Model Theory of Ordered Logics: Expressivity and Interpolation}},
booktitle = {47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
pages = {15:1--15:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-256-3},
ISSN = {1868-8969},
year = {2022},
volume = {241},
editor = {Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16813},
URN = {urn:nbn:de:0030-drops-168132},
doi = {10.4230/LIPIcs.MFCS.2022.15},
annote = {Keywords: ordered fragments, fluted fragment, guarded fragment, model theory, Craig Interpolation Property, expressive power, model checking}
}
Keywords: |
|
ordered fragments, fluted fragment, guarded fragment, model theory, Craig Interpolation Property, expressive power, model checking |
Collection: |
|
47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) |
Issue Date: |
|
2022 |
Date of publication: |
|
22.08.2022 |