一句话：证明全二叉树上 MSO 公式的良基见证序数秩要么小于 ω²，要么达到 ω₁，且可判定属于哪种情形。
论文研究全二叉树上单子二阶逻辑（MSO）公式 ∃X. φ(Y,X) 的良基见证 X 的序数秩。X 的秩 rank(X)<ω₁ 度量其深度与分支结构。作者定义 rank(φ) 为使所有满足 φ 的实例 Y 都有秩不超过 rank(φ) 的见证 X 的最小序数，并求其上界。主要结果是二分定理：对任意 φ，rank(φ) 要么严格小于 ω²，要么达到最大可能值 ω₁；并且可判定属于哪种情形。该结果可应用于若干序数相关问题，尤其可推出关于某个不动点公式闭包序数的结论。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{NiwinskiPS25,
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}
}