Order-Invariance in the Two-Variable Fragment of First-Order Logic

Author Julien Grange

Thumbnail PDF


  • Filesize: 0.77 MB
  • 19 pages

Document Identifiers

Author Details

Julien Grange
  • LACL, Université Paris-Est Créteil, France

Cite AsGet BibTex

Julien Grange. Order-Invariance in the Two-Variable Fragment of First-Order Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


We study the expressive power of the two-variable fragment of order-invariant first-order logic. This logic departs from first-order logic in two ways: first, formulas are only allowed to quantify over two variables. Second, formulas can use an additional binary relation, which is interpreted in the structures under scrutiny as a linear order, provided that the truth value of a sentence over a finite structure never depends on which linear order is chosen on its domain. We prove that on classes of structures of bounded degree, any property expressible in this logic is definable in first-order logic. We then show that the situation remains the same when we add counting quantifiers to this logic.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
  • Finite model theory
  • Two-variable logic
  • Order-invariance


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


  1. Albert Atserias, Anuj Dawar, and Martin Grohe. Preservation under extensions on well-behaved finite structures. SIAM Journal on Computing, 2008. Google Scholar
  2. Bartosz Bednarczyk. Personal communication, July 2022. Google Scholar
  3. Michael Benedikt and Luc Segoufin. Towards a characterization of order-invariant queries over tame graphs. J. Symb. Log., 2009. Google Scholar
  4. Ronald Fagin, Larry J. Stockmeyer, and Moshe Y. Vardi. On monadic NP vs. monadic co-NP. Inf. Comput., 1995. Google Scholar
  5. Erich Grädel and Martin Otto. On logics with two variables. Theor. Comput. Sci., 1999. Google Scholar
  6. Erich Grädel, Martin Otto, and Eric Rosen. Two-variable logic with counting is decidable. In LICS, 1997. Google Scholar
  7. Julien Grange. Successor-invariant first-order logic on classes of bounded degree. Log. Methods Comput. Sci., 2021. Google Scholar
  8. Julien Grange and Luc Segoufin. Order-Invariant First-Order Logic over Hollow Trees. In Computer Science Logic, CSL, 2020. Google Scholar
  9. Martin Grohe and Thomas Schwentick. Locality of order-invariant first-order formulas. ACM Trans. Comput. Log., 2000. URL: https://doi.org/10.1145/343369.343386.
  10. Neil Immerman. Relational queries computable in polynomial time. Information and Control, 1986. Google Scholar
  11. Neil Immerman and Dexter Kozen. Definability with bounded number of bound variables. Inf. Comput., 1989. Google Scholar
  12. Neil Immerman and Eric Lander. Describing graphs: A first-order approach to graph canonization. In Complexity theory retrospective. Springer, 1990. Google Scholar
  13. 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.
  14. Michael Mortimer. On languages with two variables. Math. Log. Q., 1975. Google Scholar
  15. Ian Pratt-Hartmann. Complexity of the guarded two-variable fragment with counting quantifiers. J. Log. Comput., 2007. Google Scholar
  16. Ian Pratt-Hartmann. The two-variable fragment with counting revisited. In WoLLIC, 2010. Google Scholar
  17. Moshe Y. Vardi. The complexity of relational query languages. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing, 1982. Google Scholar
  18. Philipp Weis and Neil Immerman. Structure theorem and strict alternation hierarchy for FO^2 on words. Log. Methods Comput. Sci., 2009. Google Scholar
  19. Thomas Zeume and Frederik Harwath. Order-invariance of two-variable logic is decidable. In LICS, 2016. Google Scholar