Decidability of Predicate Logics with Team Semantics

Authors Juha Kontinen, Antti Kuusisto, Jonni Virtema

Thumbnail PDF


  • Filesize: 0.53 MB
  • 14 pages

Document Identifiers

Author Details

Juha Kontinen
Antti Kuusisto
Jonni Virtema

Cite AsGet BibTex

Juha Kontinen, Antti Kuusisto, and Jonni Virtema. Decidability of Predicate Logics with Team Semantics. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 60:1-60:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


We study the complexity of predicate logics based on team semantics. We show that the satisfiability problems of two-variable independence logic and inclusion logic are both NEXPTIME-complete. Furthermore, we show that the validity problem of two-variable dependence logic is undecidable, thereby solving an open problem from the team semantics literature. We also briefly analyse the complexity of the Bernays-Schoenfinkel-Ramsey prefix classes of dependence logic.
  • team semantics
  • dependence logic
  • complexity
  • two-variable logic


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


  1. Saguy Benaim, Michael Benedikt, Witold Charatonik, Emanuel Kieroński, Rastislav Lenhardt, Filip Mazowiecki, and James Worrell. Complexity of two-variable logic on finite trees. In ICALP (2), pages 74-88, 2013. URL:
  2. R. Berger. The undecidability of the domino problem. Memoirs of the American Mathematical Society, 66:369-395, 1966. Google Scholar
  3. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997. Google Scholar
  4. Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and trees. In LICS, pages 73-82. IEEE Computer Society, 2013. URL:
  5. A. Durand, J. Kontinen, and H. Vollmer. Expressivity and Complexity of Dependence Logic, in Dependence Logic: Theory and Applications. Springer, In Press, 2016. Google Scholar
  6. Pietro Galliani. Inclusion and exclusion dependencies in team semantics - on some logics of imperfect information. Ann. Pure Appl. Logic, 163(1):68-84, 2012. URL:
  7. Pietro Galliani and Lauri Hella. Inclusion logic and fixed point logic. In proceedings of CSL 2013, pages 281-295, 2013. Google Scholar
  8. Erich Grädel. Model-checking games for logics of imperfect information. Theor. Comput. Sci., 493:2-14, 2013. URL:
  9. 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:
  10. Erich Grädel, Martin Otto, and Eric Rosen. Undecidability results on two-variable logics. In Proceedings of STACS'97, pages 249-260, London, UK, 1997. Springer-Verlag. Google Scholar
  11. Erich Grädel and Jouko Väänänen. Dependence and independence. Studia Logica, 101(2):399-410, 2013. URL:
  12. Miika Hannula. Hierarchies in inclusion logic with lax semantics. In Mohua Banerjee and Shankara Narayanan Krishna, editors, Logic and Its Applications: 6th Indian Conference, ICLA 2015, Mumbai, India, January 8-10, 2015. Proceedings, pages 100-118, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. URL:
  13. Lauri Hella and Antti Kuusisto. One-dimensional fragment of first-order logic. In Advances in Modal Logic 10, invited and contributed papers from the tenth conference on "Advances in Modal Logic," held in Groningen, The Netherlands, August 5-8, 2014, pages 274-293, 2014. URL:
  14. Jaakko Hintikka and Gabriel Sandu. Informational independence as a semantical phenomenon. In J. E. Fenstad, I. T. Frolov, and R. Hilpinen, editors, Logic, Methodology and Philosophy of Science VIII, volume 126, pages 571-589. Elsevier, Amsterdam, 1989. Google Scholar
  15. Wilfrid Hodges. Compositional semantics for a language of imperfect information. Log. J. IGPL, 5(4):539-563 (electronic), 1997. Google Scholar
  16. Emanuel Kieroński, Jakub Michaliszyn, Ian Pratt-Hartmann, and Lidia Tendera. Two-variable first-order logic with equivalence closure. SIAM Journal of Computing, 43(3):1012-1063, 2014. Google Scholar
  17. Jarmo Kontinen. Coherence and computational complexity of quantifier-free dependence logic formulas. Studia Logica, 101(2):267-291, 2013. URL:
  18. Juha Kontinen, Antti Kuusisto, Peter Lohmann, and Jonni Virtema. Complexity of two-variable dependence logic and IF-logic. Inf. Comput., 239:237-253, 2014. URL:
  19. Juha Kontinen, Antti Kuusisto, and Jonni Virtema. Decidability of predicate logics with team semantics. CoRR, abs/1410.5037, 2016. URL:
  20. Antti Kuusisto. A double team semantics for generalized quantifiers. Journal of Logic, Language and Information, 24(2):149-191, 2015. URL:
  21. Per Lindström. First order predicate logic with generalized quantifiers. Theoria, 32:186-195, 1966. Google Scholar
  22. Leszek Pacholski, Wieslaw Szwast, and Lidia Tendera. Complexity of two-variable logic with counting. In Proceedings of LICS'97, pages 318-327, 1997. URL:
  23. Ian Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. Journal of Logic, Language and Information, 14(3):369-395, 2005. URL:
  24. Wieslaw Szwast and Lidia Tendera. FO² with one transitive relation is decidable. In STACS, pages 317-328, 2013. Google Scholar
  25. Jouko Väänänen. Dependence logic: A new approach to independence friendly logic. Number 70 in London Mathematical Society student texts. Cambridge University Press, 2007. Google Scholar
  26. Jonni Virtema. Approaches to Finite Variable Dependence: Expressiveness and Computational Complexity. PhD thesis, University of Tampere, 2014. Google Scholar