We focus on formulae $\exists X.\, φ(\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 $φ$. Let $\mathrm{rank}(φ)$ 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}(φ)$. Then $\mathrm{rank}(φ)$ 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.

@article{paperbot3964,
  title = {A Dichotomy Theorem for Ordinal Ranks in MSO},
  author = {Damian Niwiński and Paweł Parys and Michał Skrzypczak},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 22, Issue 3},
  year = {2026},
  doi = {10.46298/lmcs-22(3:8)2026}
}