A Dichotomy Theorem for Ordinal Ranks in MSO

We focus on formulae ∃ X.\, φ(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 rank(X) < ω₁ 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 rank(φ) be the minimal ordinal such that, whenever an instance Y⃗ satisfies the formula, there is a witness X with rank(X) ≤ rank(φ). Then rank(φ) is either strictly smaller than ω² or it reaches the maximal possible value ω₁. 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.