A Dichotomy Theorem for Ordinal Ranks in MSO

Abstract

We focus on formulae $\exists X.\phi (\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)<{\omega }_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 $\phi$. Let $\mathrm{rank}(\phi )$ be the minimal ordinal such that, whenever an instance $\vec{Y}$ satisfies the formula, there is a witness $X$ with $\mathrm{rank}(X)\le \mathrm{rank}(\phi )$. Then $\mathrm{rank}(\phi )$ is either strictly smaller than ${\omega }^2$ or it reaches the maximal possible value ${\omega }_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.