Connecting Decidability and Complexity for MSO Logic

  • Michał SkrzypczakEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10396)


This work is about studying reasons for (un)decidability of variants of Monadic Second-order (mso) logic over infinite structures. Thus, it focuses on connecting the fact that a given theory is (un)decidable with certain measures of complexity of that theory.

The first of the measures is the topological complexity. In that case, it turns out that there are strong connections between high topological complexity of languages available in a given logic, and its undecidability. One of the milestone results in this context is the Shelah’s proof of undecidability of mso over reals.

The second complexity measure focuses on the axiomatic strength needed to actually prove decidability of the given theory. The idea is to apply techniques of reverse mathematics to the classical decidability results from automata theory. Recently, both crucial theorems of the area (the results of Büchi and Rabin) have been characterised in these terms. In both cases the proof gives strong relations between decidability of the mso theory with concepts of classical mathematics: determinacy, Ramsey theorems, weak Konig’s lemma, etc.


Monadic second-order logic Decidability Descriptive set theory Reverse mathematics 


  1. 1.
    Blumensath, A., Colcombet, T., Parys, P.: On a fragment of AMSO and tiling systems. In: STACS, pp. 19:1–19:14 (2016)Google Scholar
  2. 2.
    Bojańczyk, M.: A bounding quantifier. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 41–55. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-30124-0_7 CrossRefGoogle Scholar
  3. 3.
    Bojańczyk, M.: Weak MSO with the unbounding quantifier. Theor. Comput. Syst. 48(3), 554–576 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Bojańczyk, M.: Weak MSO+U with path quantifiers over infinite trees. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8573, pp. 38–49. Springer, Heidelberg (2014). doi: 10.1007/978-3-662-43951-7_4 Google Scholar
  5. 5.
    Bojańczyk, M., Colcombet, T.: Bounds in \(\omega \)-regularity. In: LICS, pp. 285–296 (2006)Google Scholar
  6. 6.
    Bojańczyk, M., Gogacz, T., Michalewski, H., Skrzypczak, M.: On the decidability of MSO+U on infinite trees. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8573, pp. 50–61. Springer, Heidelberg (2014). doi: 10.1007/978-3-662-43951-7_5 Google Scholar
  7. 7.
    Bojańczyk, M., Parys, P., Toruńczyk, S.: The MSO+U theory of (n, \(<\)) is undecidable. In: STACS, pp. 1–8 (2016)Google Scholar
  8. 8.
    Bojańczyk, M., Toruńczyk, S.: Deterministic automata and extensions of weak MSO. In: FSTTCS, pp. 73–84 (2009)Google Scholar
  9. 9.
    Büchi, J.R.: On a decision method in restricted second-order arithmetic. In: Lane, S.M., Siefkes, D. (eds.) The Collected Works of J. Richard Büchi, pp. 1–11. Springer, New York (1962)Google Scholar
  10. 10.
    Carayol, A., Löding, C., Niwiński, D., Walukiewicz, I.: Choice functions and well-orderings over the infinite binary tree. Cent. Europ. J. of Math. 8, 662–682 (2010)MathSciNetzbMATHGoogle Scholar
  11. 11.
    Carton, O., Colcombet, T., Puppis, G.: Regular languages of words over countable linear orderings. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 125–136. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22012-8_9 CrossRefGoogle Scholar
  12. 12.
    Friedman, H.: Some systems of second order arithmetic and their use. pp. 235–242 (1975)Google Scholar
  13. 13.
    Gödel, K.: The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory. Princeton University Press, New Jersy (1940)zbMATHGoogle Scholar
  14. 14.
    Gogacz, T., Michalewski, H., Mio, M., Skrzypczak, M.: Measure properties of game tree languages. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014. LNCS, vol. 8634, pp. 303–314. Springer, Heidelberg (2014). doi: 10.1007/978-3-662-44522-8_26 Google Scholar
  15. 15.
    Gurevich, Y., Shelah, S.: Monadic theory of order and topology in ZFC. Annal. Math. Logic 23(2–3), 179–198 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Hummel, S., Skrzypczak, M.: The topological complexity of MSO+U and related automata models. Fundam. Inf. 119(1), 87–111 (2012)MathSciNetzbMATHGoogle Scholar
  17. 17.
    Jech, T.: Set Theory. Springer, Hiedelberg (2002)zbMATHGoogle Scholar
  18. 18.
    Kechris, A.: Classical descriptive set theory. Springer, New York (1995)CrossRefzbMATHGoogle Scholar
  19. 19.
    Kolmogorov, A.N.: Operations sur des ensembles. Mat. Sb. 35, 415–422 (1928). (in Russian, summary in French)Google Scholar
  20. 20.
    Kołodziejczyk, L.A., Michalewski, H.: How unprovable is Rabin’s decidability theorem? In: LICS, pp. 788–797 (2016)Google Scholar
  21. 21.
    Kołodziejczyk, L.A., Michalewski, H., Pradic, P., Skrzypczak, M.: The logical strength of Büchi’s decidability theorem. In: CSL, pp. 36:1–36:16 (2016)Google Scholar
  22. 22.
    Liu, J.: \({\sf RT}^{2}_{2}\) does not imply \({\sf WKL}_{0}\). J. Symbol. Logic 77(2), 609–620 (2012)CrossRefGoogle Scholar
  23. 23.
    McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Inf. Control 9(5), 521–530 (1966)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1–35 (1969)MathSciNetzbMATHGoogle Scholar
  25. 25.
    Rabinovich, A.: On decidability of monadic logic of order over the naturals extended by monadic predicates. Inf. Comput. 205(6), 870–889 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Shelah, S.: The monadic theory of order. Annal. Math. 102(3), 379–419 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Simpson, S.G.: Subsystems of Second Order Arithmetic. Perspectives in Logic, 2nd edn. Cambridge University Press, Association for Symbolic Logic, Cambridge, Poughkeepsie (2009)CrossRefzbMATHGoogle Scholar
  28. 28.
    Thomas, W., Lescow, H.: Logical specifications of infinite computations. In: Bakker, J.W., Roever, W.-P., Rozenberg, G. (eds.) REX 1993. LNCS, vol. 803, pp. 583–621. Springer, Heidelberg (1994). doi: 10.1007/3-540-58043-3_29 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.University of WarsawWarsawPoland

Personalised recommendations