Document Open Access Logo

The Uniformisation of Monadic Second-Order Logic over Countable Ordinals

Authors Thomas Colcombet , Alexander Rabinovich

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.30.pdf
  • Filesize: 0.97 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Monadic second-order logic
  • uniformisation
  • chains
  • ordinals
  • composition method
  • factorization trees

Metrics

Abstract

We study the uniformisation problem for monadic second-order logic (MSO) over countable ordinal chains. Given a formula defining a relation between subsets of the input structure, the question is whether there exists a formula that defines a function selecting, for every set in the domain of the relation, a unique set such that the pair belongs to the relation. It is known, due to Lifsches and Shelah [Lifsches and Shelah, 1998], that MSO cannot, in general, be uniformised over the class of countable ordinals.
We show that the maximal uniformisation degree is reached by extending the logic with a predicate that, given a set, selects (when possible) a cofinal subset of order type ω. Equivalently, every MSO formula can be uniformised over the class of countable ordinal chains using a formula in this extended logic.

Cite As Get BibTex

Thomas Colcombet and Alexander Rabinovich. The Uniformisation of Monadic Second-Order Logic over Countable Ordinals. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 30:1-30:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.30

Author Details

Thomas Colcombet
  • CNRS, IRIF, Université Paris Cité, France
Alexander Rabinovich
  • The Blavatnik School of CS and AI, 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é, and supported in part by Len Blavatnik and the Blavatnik Family foundation.

References

  1. Green J. A. On the structure of semigroups. Annals of Mathematics, 54(1):163-172, 1951. URL: https://doi.org/10.2307/1969317.
  2. Nicolas Bedon and Olivier Carton. An eilenberg theorem for words on countable ordinals. In LATIN, volume 1380 of Lecture Notes in Computer Science, pages 53-64. Springer, 1998. URL: https://doi.org/10.1007/BFB0054310.
  3. J. Richard Buchi and Dirk Siefkes. The Monadic Second Order Theory of All Countable Ordinals, volume 328 of Lecture Notes in Mathematics. Springer, 2006. Reprint of the 1973 edition. Google Scholar
  4. Arnaud Carayol, Christof Löding, Damian Niwiński, and Igor Walukiewicz. Choice functions and well-orderings over the infinite binary tree. Central European Journal of Mathematics, 8(3):503-521, 2010. URL: https://doi.org/10.2478/s11533-010-0033-4.
  5. Olivier Carton, Thomas Colcombet, and Gabriele Puppis. An algebraic approach to MSO-definability on countable linear orderings. Journal of Symbolic Logic, 83(3):1147-1189, 2018. URL: https://doi.org/10.1017/jsl.2018.7.
  6. Thomas Colcombet. Factorization forests for infinite words and applications. Theoretical Computer Science, 411(4-5):751-764, 2010. URL: https://doi.org/10.1016/j.tcs.2009.10.013.
  7. Krzysztof Fabiański, Michał Skrzypczak, and Paweł Szymoński. Deciding regular uniformization over z-words. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), pages 431-444. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394739.
  8. Nathan Lhote, Matteo Michielini, and Michał Skrzypczak. Uniformization property for automatic relations. In Mathematical Foundations of Computer Science (MFCS 2019), volume 138 of LIPIcs, pages 67:1-67:15. Schloss Dagstuhl, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.67.
  9. Shmuel Lifsches and Saharon Shelah. Uniformization and skolem functions in the class of trees. The Journal of Symbolic Logic, 63(1):103-127, 1998. URL: https://doi.org/10.2307/2586591.
  10. Matteo Michielini. Uniformization problems for relations over infinite words. In Developments in Language Theory (DLT 2018), volume 11088 of Lecture Notes in Computer Science, pages 258-270. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98654-8_22.
  11. Matteo Michielini and Michał Skrzypczak. Regular uniformizations over infinite linear orders. In Mathematical Foundations of Computer Science (MFCS 2020), volume 170 of LIPIcs, pages 71:1-71:14. Schloss Dagstuhl, 2020. URL: https://doi.org/10.4230/LIPIcs.MFCS.2020.71.
  12. Alexander Rabinovich. Rabin uniformization problem with restricted domain variables. In Guillermo Badia, Manfred Droste, Andreas Blass, and Nachum Dershowitz, editors, Fields of Logic and Computation IV: Essays Dedicated to Yuri Gurevich, Lecture Notes in Computer Science. Springer, to appear. Google Scholar
  13. Alexander Rabinovich and Amit Shomrat. Selection in the monadic theory of a countable ordinal. Journal of Symbolic Logic, 73(3):783-816, 2008. URL: https://doi.org/10.2178/jsl/1230396747.
  14. Alexander Rabinovich and Amit Shomrat. Selection over classes of ordinals expanded by monadic predicates. Annals of Pure and Applied Logic, 161(8):1006-1023, 2010. URL: https://doi.org/10.1016/j.apal.2009.12.004.
  15. Imre Simon. Factorization forests of finite height. In ICALP'90: Proceedings of the 17th International Colloquium on Automata, Languages and Programming, volume 443 of Lecture Notes in Computer Science, pages 392-403. Springer, 1990. URL: https://doi.org/10.1007/BFb0032058.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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