Document Open Access Logo

Towards a Model Theory of Ordered Logics: Expressivity and Interpolation

Authors Bartosz Bednarczyk , Reijo Jaakkola

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2022.15.pdf
  • Filesize: 0.82 MB
  • 14 pages

Document Identifiers

Author Details

Bartosz Bednarczyk
  • Computational Logic Group, Technische Universität Dresden, Germany
  • Institute of Computer Science, University of Wrocław, Poland
Reijo Jaakkola
  • Tampere University, Finland

Funding

  • Bednarczyk, Bartosz: supported by the ERC Consolidator Grant No. 771779 (DeciGUT).

Acknowledgements

We would like to thank Antti Kuusisto and Jean Christoph Jung for fruitful discussions on related topics, as well as Tim Lyon and Emanuel Kieroński for language corrections. We would also like to thank the anonymous reviewers for their very helpful comments.

Cite AsGet BibTex

Bartosz Bednarczyk and Reijo Jaakkola. Towards a Model Theory of Ordered Logics: Expressivity and Interpolation. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.15

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
Keywords
  • ordered fragments
  • fluted fragment
  • guarded fragment
  • model theory
  • Craig Interpolation Property
  • expressive power
  • model checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Hajnal Andréka, István Németi, and Johan van Benthem. Modal Languages and Bounded Fragments of Predicate Logic. J. Philos. Log., 1998. Google Scholar
  2. Vince Bárány, Michael Benedikt, and Balder ten Cate. Some Model Theory of Guarded Negation. J. Symb. Log., 2018. Google Scholar
  3. Vince Bárány, Balder ten Cate, and Luc Segoufin. Guarded Negation. J. ACM, 2015. Google Scholar
  4. Bartosz Bednarczyk. Exploiting Forwardness: Satisfiability and Query-Entailment in Forward Guarded Fragment. In JELIA, 2021. Google Scholar
  5. Bartosz Bednarczyk and Reijo Jaakkola. Towards a model theory of ordered logics: Expressivity and interpolation (extended version), arXiV 2022. URL: https://doi.org/10.48550/ARXIV.2206.11751.
  6. Michael Benedikt, Balder ten Cate, and Michael Vanden Boom. Effective Interpolation and Preservation in Guarded Logics. ACM Trans. Comput. Log., 2016. Google Scholar
  7. Dietmar Berwanger and Erich Graedel. Games and Model Checking for Guarded Logics. In LPAR 2001, 2001. Google Scholar
  8. Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. Bull. Symb. Log., 1997. Google Scholar
  9. Erich Grädel and Martin Otto. The Freedoms of (Guarded) Bisimulation. In Alexandru Baltag and Sonja Smets, editors, Johan van Benthem on Logic and Information Dynamics. Springer, 2014. Google Scholar
  10. Erich Graedel, Phokion Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, and Scott Weinstein. Finite Model Theory and Its Applications. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2007. Google Scholar
  11. Lauri Hella and Antti Kuusisto. One-dimensional Fragment of First-order Logic. In AIML 2014, 2014. Google Scholar
  12. Andreas Herzig. A New Decidable Fragment of First Order Logic. In Third Logical Biennial, Summer School and Conference in Honour of S. C. Kleene, 1990. Google Scholar
  13. Wilfrid Hodges. A Shorter Model Theory. Cambridge University Press, 1997. Google Scholar
  14. Eva Hoogland, Maarten Marx, and Martin Otto. Beth Definability for the Guarded Fragment. In LPAR, 1999. Google Scholar
  15. Reijo Jaakkola. Ordered Fragments of First-Order Logic. In MFCS, 2021. Google Scholar
  16. Reijo Jaakkola. Uniform Guarded Fragments. In FOSSACS, 2022. Google Scholar
  17. Jean Christoph Jung and Frank Wolter. Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments. In LICS, 2021. Google Scholar
  18. Leonid Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-07003-1.
  19. Maarten Marx. Algebraic relativization and arrow logic. University of Amsterdam, 1995. Google Scholar
  20. Ian Pratt-Hartmann, Wieslaw Szwast, and Lidia Tendera. The Fluted Fragment Revisited. J. Symb. Log., 2019. Google Scholar
  21. William C. Purdy. Complexity and Nicety of Fluted Logic. Stud Logica, 2002. Google Scholar
  22. Willard Quine. The Ways of Paradox and Other Essays, Revised Edition. Harvard University Press, 1976. Google Scholar
  23. Abraham Robinson. A Result on Consistency and Its Application to the Theory of Definition. Journal of Symbolic Logic, 1960. Google Scholar
  24. Luc Segoufin and Balder ten Cate. Unary negation. Log. Methods Comput. Sci., 9(3), 2013. Google Scholar
  25. Thomas Sturm, Marco Voigt, and Christoph Weidenbach. Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. In LICS 2016, 2016. Google Scholar
  26. Johan van Benthem. Modal Foundations for Predicate Logic. Log. J. IGPL, 1997. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact