A Dichotomy Theorem for Ordinal Ranks in MSO

Damian NiwiÅski; PaweÅ Parys; MichaÅ Skrzypczak

logic in computer science

A Dichotomy Theorem for Ordinal Ranks in MSO

arXiv:2501.05385

summary

The paper investigates monadic second‑order formulas over the full binary tree that require a well‑founded witness set, defines an ordinal rank for such sets, and proves a decidable dichotomy: the minimal rank needed is either below ω² or reaches the maximal value ω₁.

Abstract

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

Full version of a STACS 2025 paper, see doi:10.4230/LIPIcs.STACS.2025.64 Updated in Oct-Dec 2025 towards the journal version

Topics & keywords

#monadic second-order logic #ordinal ranks #binary tree #decidability #fixed-point logicMSOordinal rankwell‑founded setω²ω₁closure ordinal