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

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.