Document Open Access Logo

On the Expansion of Monadic Second-Order Logic with Cantor-Bendixson Rank and Order Type Predicates

Authors Thomas Colcombet , Alexander Rabinovich

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2025.11.pdf
  • Filesize: 1.05 MB
  • 26 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Tree languages
  • Theory of computation → Logic and verification
Keywords
  • Logic
  • Algorithmic model theory
  • Monadic second-order logic
  • Ordinals
  • Binary tree

Metrics

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

Abstract

In this work, we consider two extensions of monadic second-order logic, and study in what cases the classical decidability results are preserved.
The first extension, MSO[CBrank_β], is MSO (over the signature of the binary tree) augmented with the extra ability to express that the subtree over a set X has Cantor-Bendixson rank β, for some fixed countable ordinal β. We show that this extension is decidable over the binary tree if and only if β is finite, which means that it is decidable if and only if it is equivalent in expressiveness to MSO.
The second extension, MSO[otp_α], is MSO (over the signature of order) augmented with the extra ability to express that the suborder induced by a set X has order type α for some fixed countable ordinal α. We show that this extension is decidable over countable ordinals if and only if α < ω^ω, which means that it is decidable if and only if it is equivalent in expressiveness to MSO.
The first result can be established as a consequence of the second. The second result relies on the undecidability results of the logic BMSO (itself relying on the undecidability of MSO+U) in the case of ω^β for β a limit ordinal, and on entirely new techniques when β is a successor ordinal. We also have some partial extensions of the second result to some uncountable cases.

Cite As Get BibTex

Thomas Colcombet and Alexander Rabinovich. On the Expansion of Monadic Second-Order Logic with Cantor-Bendixson Rank and Order Type Predicates. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 11:1-11:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.11

Author Details

Thomas Colcombet
  • Université Paris Cité, CNRS, IRIF, France
Alexander Rabinovich
  • The Blavatnik School of Computer Science, Tel-Aviv University, Israel

Funding

  • Rabinovich, Alexander: Visits to IRIF were supported by the Fondation Sciences Mathématiques de Paris (FSMP) and Université Paris Cité.

References

  1. Valérie Berthé, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, and James Worrell. On the decidability of monadic second-order logic with arithmetic predicates. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 11:1-11:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662119.
  2. Achim Blumensath, Olivier Carton, and Thomas Colcombet. Asymptotic monadic second-order logic. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, volume 8634 of Lecture Notes in Computer Science, pages 87-98. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44522-8_8.
  3. Achim Blumensath, Thomas Colcombet, Denis Kuperberg, Pawel Parys, and Michael Vanden Boom. Two-way cost automata and cost logics over infinite trees. 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 16:1-16:9. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603104.
  4. Mikolaj Bojanczyk. A bounding quantifier. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 41-55. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30124-0_7.
  5. Mikolaj Bojanczyk and Thomas Colcombet. Boundedness in languages of infinite words. Log. Methods Comput. Sci., 13(4), 2017. URL: https://doi.org/10.23638/LMCS-13(4:3)2017.
  6. Mikolaj Bojanczyk, Laure Daviaud, Bruno Guillon, Vincent Penelle, and A. V. Sreejith. Undecidability of a weak version of MSO+U. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:12)2020.
  7. Mikolaj Bojanczyk, Edon Kelmendi, Rafal Stefanski, and Georg Zetzsche. Extensions of ω-regular languages. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 266-272. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394779.
  8. Mikolaj Bojanczyk, Pawel Parys, and Szymon Torunczyk. The MSO+U theory of (n, less) is undecidable. In Nicolas Ollinger and Heribert Vollmer, editors, 33rd Symposium on Theoretical Aspects of Computer Science, STACS 2016, February 17-20, 2016, Orléans, France, volume 47 of LIPIcs, pages 21:1-21:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.STACS.2016.21.
  9. Mikolaj Bojanczyk and Szymon Torunczyk. Weak MSO+U over infinite trees. In Christoph Dürr and Thomas Wilke, editors, 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France, volume 14 of LIPIcs, pages 648-660. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.STACS.2012.648.
  10. J. R. Büchi. On a decision method in the restricted second-order arithmetic. In Proc. Int. Congress Logic, Methodology and Philosophy of science, Berkeley 1960, pages 1-11. Stanford University Press, 1962. Google Scholar
  11. J. R. Büchi. Transfinite automata recursions and weak second order theory of ordinals. In Proc. Int. Congress Logic, Methodology, and Philosophy of Science, Jerusalem 1964, pages 2-23. HOLLAND, 1965. Google Scholar
  12. J Richard Büchi and Dirk Siefkes. Decidable Theories: Vol. 2: The Monadic Second Order Theory of All Countable Ordinals, volume 328. Springer, 2006. Google Scholar
  13. J.Richard Büchi and Charles Zaiontz. Deterministic automata and the monadic theory of ordinals ω_2. Z. Math. Logik Grundlagen Math., 29:313-336, 1983. Google Scholar
  14. O. Carton and W. Thomas. The monadic theory of morphic infinite words and generalizations. Inform. Comput., 176:51-76, 2002. Google Scholar
  15. Thomas Colcombet. Regular cost functions, part I: logic and algebra over words. Log. Methods Comput. Sci., 9(3), 2013. URL: https://doi.org/10.2168/LMCS-9(3:3)2013.
  16. Thomas Colcombet and Christof Löding. Regular cost functions over finite trees. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 70-79. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/LICS.2010.36.
  17. Calvin C. Elgot and Michael O. Rabin. Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. J. Symb. Log., 31(2):169-181, 1966. URL: https://doi.org/10.2307/2269808.
  18. S. Fratani. The theory of successor extended with several predicates. preprint, 2009. Google Scholar
  19. Y. Gurevich. Monadic second-order theories. In J. Barwise and S. Feferman, editors, Model-Theoretic Logics, pages 479-506. Springer-Verlag, Perspectives in Mathematical Logic, 1985. Google Scholar
  20. Yuri Gurevich. Modest theory of short chains. i. J. Symb. Log., 44(4):481-490, 1979. URL: https://doi.org/10.2307/2273287.
  21. Yuri Gurevich, Menachem Magidor, and Saharon Shelah. The monadic theory of ω₂. J. Symb. Log, 48(2):387-398, 1983. Google Scholar
  22. Yuri Gurevich and Saharon Shelah. Modest theory of short chains. ii. J. Symb. Log., 44(4):491-502, 1979. URL: https://doi.org/10.2307/2273288.
  23. Yuri Gurevich and Saharon Shelah. Interpreting second-order logic in the monadic theory of order. J. Symb. Log., 48(3):816-828, 1983. URL: https://doi.org/10.2307/2273475.
  24. M.O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1-35, 1969. Google Scholar
  25. A. Rabinovich. On decidability of monadic logic of order over the naturals extended by monadic predicates. Inf. Comput, 205(6):870-889, 2007. URL: https://doi.org/10.1016/J.IC.2006.12.004.
  26. A. Rabinovich and W. Thomas. Decidable theories of the ordering of natural numbers with unary predicates. In Zoltán Ésik, editor, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pages 562-574. Springer, 2006. URL: https://doi.org/10.1007/11874683_37.
  27. R.M. Robinson. Restricted set-theoretical definitions in arithmetic. Proc. Am. Math. Soc., 9:238-242, 1958. Google Scholar
  28. J.G. Rosenstein. Linear Orderings. ISSN. Elsevier Science, 1982. URL: https://books.google.com.sg/books?id=y3YpdW-sbFsC.
  29. A. L. Semenov. Decidability of monadic theories. In M. P. Chytil and V. Koubek, editors, Proceedings of the 11th Symposium on Mathematical Foundations of Computer Science, volume 176 of LNCS, pages 162-175, Praha, Czechoslovakia, September 1984. Springer. URL: https://doi.org/10.1007/BFB0030296.
  30. A. L. Semenov. Logical theories of one-place functions on the set of natural numbers. Mathematics of the USSR - Izvestia, 22:587-618, 1984. Google Scholar
  31. S. Shelah. The monadic theory of order. Annals of Mathematics, 102:379-419, 1975. Google Scholar
  32. Saharon Shelah. The monadic theory of order. The Annals of Mathematics, 102(3):379, November 1975. URL: https://doi.org/10.2307/1971037.
  33. D. Siefkes. Decidable extensions of monadic second order successor arithmetic. Automatentheorie und Formale Sprachen, (Tagung, Math. Forschungsinst, Oberwolfach), 1969; (Bibliograph. Inst., Mannheim), pages 441-472, 1970. Google Scholar
  34. W. Thomas. A note on undecidable extensions of monadic second order successor arithmetic. Arch. Math. Logik Grundlagenforsch., 17:43-44, 1975. URL: https://doi.org/10.1007/BF02280812.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact