2026-07-25T14:45:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22768 2025-02-03T10:18:30Z ddc:004 open_access

On the Expansion of Monadic Second-Order Logic with Cantor-Bendixson Rank and Order Type Predicates Colcombet, Thomas Rabinovich, Alexander Logic Algorithmic model theory Monadic second-order logic Ordinals Binary tree 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thomas Colcombet and Alexander Rabinovich 2025 Is Part Of LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2025.11 urn:nbn:de:0030-drops-227685 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.11 eng https://creativecommons.org/licenses/by/4.0/legalcode