Two Variable Logic with Ultimately Periodic Counting

Authors Michael Benedikt, Egor V. Kostylev, Tony Tan

Thumbnail PDF


  • Filesize: 0.65 MB
  • 16 pages

Document Identifiers

Author Details

Michael Benedikt
  • University of Oxford, UK
Egor V. Kostylev
  • University of Oxford, UK
Tony Tan
  • National Taiwan University, Taipei, Taiwan


We are grateful to Bartosz Bednarczyk for many useful comments and suggestions on preliminary drafts of this work.

Cite AsGet BibTex

Michael Benedikt, Egor V. Kostylev, and Tony Tan. Two Variable Logic with Ultimately Periodic Counting. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 112:1-112:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


We consider the extension of FO² with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence is definable in Presburger arithmetic. In the process we present several refinements to the "biregular graph method". In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Presburger Arithmetic
  • Two-variable logic


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


  1. Franz Baader. A new description logic with set constraints and cardinality constraints on role successors. In FROCOS, 2017. Google Scholar
  2. Bartosz Bednarczyk. One-variable logic meets Presburger arithmetic. Theor. Comput. Sci., 802:141-146, 2020. Google Scholar
  3. Bartosz Bednarczyk, Franz Baader, and Sebastian Rudolph. Satisfiability and query answering in description logics with global and local cardinality constraints. In ECAI, 2020. Google Scholar
  4. Bartosz Bednarczyk and Witold Charatonik. Modulo counting on words and trees. In FSTTCS, 2017. Google Scholar
  5. Witold Charatonik, Yegor Guskov, Ian Pratt-Hartmann, and Piotr Witkowski. Two-variable first-order logic with counting in forests. In LPAR, 2018. Google Scholar
  6. Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and trees. ACM Trans. Comput. Log., 17(4):31:1-31:27, 2016. Google Scholar
  7. Stéphane Demri and Denis Lugiez. Complexity of modal logics with Presburger constraints. J. Applied Logic, 8(3):233-252, 2010. Google Scholar
  8. Arnaud Durand, Neil D. Jones, Johann A. Makowsky, and Malika More. Fifty years of the spectrum problem: survey and new results. The Bulletin of Symbolic Logic, 18(4):505-553, 2012. Google Scholar
  9. Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. Bull. Symbolic Logic, 3(1):53-69, March 1997. Google Scholar
  10. Erich Grädel, Martin Otto, and Eric Rosen. Two-variable logic with counting is decidable. In LICS, 1997. Google Scholar
  11. Erich Grädel, Martin Otto, and Eric Rosen. Undecidability results on two-variable logics. Arch. Math. Logic, 38:313-354, 1999. Google Scholar
  12. Emanuel Kieronski, Jakub Michaliszyn, Ian Pratt-Hartmann, and Lidia Tendera. Two-variable first-order logic with equivalence closure. SIAM J. Comput., 43(3):1012-1063, 2014. Google Scholar
  13. Eryk Kopczyński and Tony Tan. Regular graphs and the spectra of two-variable logic with counting. SIAM J. Comput., 44(3):786-818, 2015. Google Scholar
  14. Viktor Kuncak and Martin C. Rinard. Towards efficient satisfiability checking for boolean algebra with Presburger arithmetic. In CADE, 2007. Google Scholar
  15. Michael Mortimer. On language with two variables. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 21:135-140, 1975. Google Scholar
  16. Leszek Pacholski, Wieslaw Szwast, and Lidia Tendera. Complexity results for first-order two-variable logic with counting. SIAM J. Comput., 29(4):1083-1117, 2000. Google Scholar
  17. Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765-768, October 1981. Google Scholar
  18. Ian Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. Journal of Logic Language and Information, 14:369-395, 2005. Google Scholar
  19. Ian Pratt-Hartmann. Complexity of the guarded two-variable fragment with counting quantifiers. J. Log. Comput., 17(1):133-155, 2007. Google Scholar
  20. Ian Pratt-Hartmann. Data-complexity of the two-variable fragment with counting quantifiers. Inf. Comput., 207(8):867-888, 2009. Google Scholar
  21. Ian Pratt-Hartmann. The two-variable fragment with counting revisited. In WoLLIC, 2010. Google Scholar
  22. Ian Pratt-Hartmann. The two-variable fragment with counting and equivalence. Math. Log. Q., 61(6):474-515, 2015. Google Scholar
  23. Dana Scott. A decision method for validity of sentences in two variables. The Journal of Symbolic Logic, page 377, 1962. Google Scholar