A Dichotomy Theorem for Ordinal Ranks in MSO

TL;DR

This paper establishes a dichotomy theorem for the ordinal ranks of well-founded witnesses in monadic second-order logic over binary trees, showing the ranks are either bounded below  or reach the supremum 

, with decidability of the case.

Contribution

It proves a dichotomy theorem for the minimal ordinal bounds of witnesses in MSO logic over binary trees, identifying when ranks are bounded or maximal, and shows this is decidable.

Findings

Ranks are either less than  or equal to 

.

Decidability of which case applies.

Potential applications to ordinal-related problems and fixed-point formulas.

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) < \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 $\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 $\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.