A Dichotomy Theorem for Ordinal Ranks in MSO
Damian Niwiński, Paweł Parys, Michał Skrzypczak
TL;DR
This work proves a sharp dichotomy for ordinal ranks of well-founded witnesses in MSO over the full binary tree: the bound rank(φ) for existential MSO witnesses is either below ω^2 or equal to ω1, with an effective method to decide which case occurs. The authors introduce a refined rank notion, rank^R, together with a finite-game framework (the dichotomy game) that characterizes when witnesses must have layered depth bounded by ω·N or can be arbitrarily large (ω1). Central to the approach are automata-theoretic translations (Rabin’s tree theorem), derivative-based rank analyses, and a game-theoretic decomposition that yields both decidability and a computable bound in the finite-case. The results connect MSO-definability, fixed-point theory, and ordinal analysis, and imply consequences for vectorial fixed points and closure ordinals, while highlighting expressibility limits within MSO and connections to μ-calculus theories.
Abstract
We focus on formulae $\exists X.\, \varphi(\vec{Y}, X)$ of monadic second-order logic over the full binary tree, such that the witness $X$ is a well-founded set. The ordinal rank $\mathrm{rank}(X) < ω_1$ of such a set $X$ measures its depth and branching structure. We search for the least upper bound for these ranks, and discover the following dichotomy depending on the formula $\varphi$. Let $\mathrm{rank}(\varphi)$ be the minimal ordinal such that, whenever an instance $\vec{Y}$ satisfies the formula, there is a witness $X$ with $\mathrm{rank}(X) \leq \mathrm{rank}(\varphi)$. Then $\mathrm{rank}(\varphi)$ is either strictly smaller than $ω^2$ or it reaches the maximal possible value $ω_1$. Moreover, it is decidable which of the cases holds. The result has potential for applications in a variety of ordinal-related problems, in particular it entails a result about the closure ordinal of a fixed-point formula.