Document

# On the Limits of Decision: the Adjacent Fragment of First-Order Logic

## File

LIPIcs.ICALP.2023.111.pdf
• Filesize: 0.89 MB
• 21 pages

## Acknowledgements

B. Bednarczyk thanks R. Jaakkola for many inspiring discussions.

## Cite As

Bartosz Bednarczyk, Daumantas Kojelis, and Ian Pratt-Hartmann. On the Limits of Decision: the Adjacent Fragment of First-Order Logic. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 111:1-111:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ICALP.2023.111

## Abstract

We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that its satisfiability problem is no harder than for the fluted fragment (and hence is Tower-complete). We further show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable. Finally, we study the effect of the adjacency requirement on the well-known guarded fragment (GF) of first-order logic. We show that the satisfiability problem for the guarded adjacent fragment (GA) remains 2ExpTime-hard, thus strengthening the known lower bound for GF.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Finite Model Theory
##### Keywords
• decidability
• satisfiability
• variable-ordered logics
• complexity

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Hajnal Andréka, István Németi, and Johan van Benthem. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217-274, 1998. URL: https://doi.org/10.1023/a:1004275029985.
2. Bartosz Bednarczyk. Exploiting forwardness: Satisfiability and query-entailment in forward guarded fragment. In Wolfgang Faber, Gerhard Friedrich, Martin Gebser, and Michael Morak, editors, Logics in Artificial Intelligence - 17th European Conference, JELIA 2021, Virtual Event, May 17-20, 2021, Proceedings, volume 12678 of Lecture Notes in Computer Science, pages 179-193. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-75775-5_13.
3. Bartosz Bednarczyk, Witold Charatonik, and Emanuel Kieroński. Extending two-variable logic on trees. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden, volume 82 of LIPIcs, pages 11:1-11:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.11.
4. Bartosz Bednarczyk and Reijo Jaakkola. Towards a model theory of ordered logics: Expressivity and interpolation. In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria, volume 241 of LIPIcs, pages 15:1-15:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.15.
5. Bartosz Bednarczyk, Daumantas Kojelis, and Ian Pratt-Hartmann. On the limits of decision: the adjacent fragment of first-order logic. ArXiV, abs/2305.03133, 2023. URL: https://arxiv.org/abs/2305.03133.
6. Michael Benedikt, Egor V. Kostylev, and Tony Tan. Two variable logic with ultimately periodic counting. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 112:1-112:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.112.
7. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Transactions on Computational Logic, 12(4), July 2011. URL: https://doi.org/10.1145/1970398.1970403.
8. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997.
9. Witold Charatonik, Emanuel Kieroński, and Filip Mazowiecki. Decidability of weak logics with deterministic transitive closure. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, pages 29:1-29:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603134.
10. Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and trees. ACM Transactions on Computational Logic, 17(4), November 2016. URL: https://doi.org/10.1145/2983622.
11. Erich Grädel. On the restraining power of guards. The Journal of Symbolic Logic, 64(4):1719-1742, 1999. URL: http://www.jstor.org/stable/2586808.
12. Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. The Bulletin of Symbolic Logic, 3(1):53-69, 1997. URL: http://www.jstor.org/stable/421196.
13. Leon Henkin. Logical Systems Containing Only a Finite Number of Symbols. Séminaire de mathématiques supérieures. Presses de l'Université de Montréal, 1967. URL: https://books.google.pl/books?id=0jPQAAAAMAAJ.
14. Andreas Herzig. A new decidable fragment of first order logic. In Abstracts of the 3rd Logical Biennial Summer School and Conference in honour of S. C. Kleene, Varna, Bulgaria, June 1990.
15. David Hilbert and Wilhelm Ackermann. Grundzüge der theoretischen Logik. Springer, Berlin, 1928.
16. David Hilbert and Wilhelm Ackermann. Principles of Mathematical Logic. Chelsea, New York, 1950.
17. Ullrich Hustadt, Renate A Schmidt, and Lilia Georgieva. A survey of decidable first-order fragments and description logics. Journal of Relational Methods in Computer Science, 1(3):251-276, 2004.
18. Reijo Jaakkola. Ordered fragments of first-order logic. In Filippo Bonchi and Simon J. Puglisi, editors, 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, August 23-27, 2021, Tallinn, Estonia, volume 202 of LIPIcs, pages 62:1-62:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.62.
19. Emanuel Kieroński. One-dimensional guarded fragments. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, volume 138 of LIPIcs, pages 16:1-16:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.16.
20. Emanuel Kieroński and Jakub Michaliszyn. Two-variable universal logic with transitive closure. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, volume 16 of LIPIcs, pages 396-410. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.396.
21. Emanuel Kieroński, Jakub Michaliszyn, Ian Pratt-Hartmann, and Lidia Tendera. Two-variable first-order logic with equivalence closure. SIAM Journal on Computing, 43(3):1012-1063, 2014. URL: https://doi.org/10.1137/120900095.
22. Emanuel Kieroński and Martin Otto. Small substructures and decidability issues for first-order logic with two variables. Journal of Symbolic Logic, 77(3):729-765, 2012. URL: https://doi.org/10.2178/jsl/1344862160.
23. Emanuel Kieroński, Ian Pratt-Hartmann, and Lidia Tendera. Two-variable logics with counting and semantic constraints. ACM SIGLOG News, 5(3):22-43, 2018. URL: https://doi.org/10.1145/3242953.3242958.
24. Emanuel Kieroński and Lidia Tendera. On finite satisfiability of two-variable first-order logic with equivalence relations. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 123-132. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/LICS.2009.39.
25. Amaldev Manuel. Two variables and two successors. In Petr Hlinený and Antonín Kucera, editors, Mathematical Foundations of Computer Science 2010, 35th International Symposium, MFCS 2010, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6281 of Lecture Notes in Computer Science, pages 513-524. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15155-2_45.
26. Ian Pratt-Hartmann. The two-variable fragment with counting revisited. In Anuj Dawar and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010, Brasilia, Brazil, July 6-9, 2010. Proceedings, volume 6188 of Lecture Notes in Computer Science, pages 42-54. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13824-9_4.
27. Ian Pratt-Hartmann. Finite satisfiability for two-variable, first-order logic with one transitive relation is decidable. Mathematical Logic Quarterly, 64(3):218-248, 2018. URL: https://doi.org/10.1002/malq.201700055.
28. Ian Pratt-Hartmann. Fluted logic with counting. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 141:1-141:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.141.
29. Ian Pratt-Hartmann. Walking on words. ArXiV, abs/2208.08913, 2022. URL: https://doi.org/10.48550/arXiv.2208.08913.
30. Ian Pratt-Hartmann, Wieslaw Szwast, and Lidia Tendera. The fluted fragment revisited. Journal of Symbolic Logic, 84(3):1020-1048, 2019.
31. Ian Pratt-Hartmann and Lidia Tendera. The fluted fragment with transitive relations. Annals of Pure and Applied Logic, 173(1):103042, 2022. URL: https://doi.org/10.1016/j.apal.2021.103042.
32. William C. Purdy. Fluted formulas and the limits of decidability. The Journal of Symbolic Logic, 61(2):608-620, 1996. URL: http://www.jstor.org/stable/2275678.
33. Willard Van Orman Quine. On the limits of decision. In Proceedings of the 14th International Congress of Philosophy, volume III, pages 57-62. University of Vienna, 1969.
34. Willard Van Orman Quine. Algebraic logic and predicate functors. In The Ways of Paradox, pages 283-307. Harvard University Press, Cambridge, MA, revised and enlarged edition, 1976.
35. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Transactions on Computational Logic, 8(1), February 2016. URL: https://doi.org/10.1145/2858784.
36. Thomas Schwentick and Thomas Zeume. Two-Variable Logic with Two Order Relations. Logical Methods in Computer Science, Volume 8, Issue 1, March 2012. URL: https://doi.org/10.2168/LMCS-8(1:15)2012.
37. Thomas Zeume and Frederik Harwath. Order-invariance of two-variable logic is decidable. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 807-816. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933594.