A Dichotomy Theorem for Ordinal Ranks in MSO

技术摘要：MSO 中序数秩的二分定理

1. 问题阐述

本文研究了在全无限二叉树上，单调二阶逻辑（MSO）的表达能力，特别是关于作为存在量化见证（witnesses）的良基集（well-founded sets）的复杂度。

考虑形式为 $\exists X. \varphi(\vec{Y}, X)$ 的公式，其中 $\varphi$ 是任意 MSO 公式。作者假设，每当该公式对于 $\vec{Y}$ 的某种赋值满足时，见证集 $X$ 都是良基的（即相对于树的后代序不包含无限下降链）。对于这样的集合 $X$，一个可数的序数秩（rank），记作 $\text{rank}(X)$，是定义良好的，它衡量了集合的深度和分支结构。

核心问题是确定给定公式的闭包序数（closure ordinal，或最小上界）。令 $\text{rank}(\varphi)$ 定义为：
$$\text{rank}(\varphi) \stackrel{\text{def}}{=} \sup_{\vec{Y}} \min_{X} \text{rank}(X)$$
其中上确界是对满足该公式的所有赋值 $\vec{Y}$ 取的，而最小值是对所有见证集 $X$ 取的。由于可数序数的上确界至多为 $\omega_1$（第一个不可数序数），因此问题在于：$\text{rank}(\varphi)$ 的精确值是多少？

先前的研究已经证明，对于任何自然数对 $(k, l)$，都可以构造出一个满足 $\text{rank}(\varphi) = \omega \cdot k + l$ 的公式。然而，此前尚不清楚是否存在其他序数（特别是那些 $\ge \omega^2$ 但 $< \omega_1$ 的序数）可以作为 MSO 公式的闭包序数实现。

2. 研究方法

作者结合自动机理论，采用了一种博弈论方法来刻画这些秩。

• 自动机表示： 作者并没有直接处理 MSO 公式，而是利用了 MSO 与非确定性 Parity 树自动机之间的等价性（Rabin 定理）。他们定义了一个由剪枝自动机（pruned automaton）识别的正规关系 $\Gamma \subseteq \text{Tr}_A \times \text{WF}$（其中 $\text{WF}$ 是良基树的集合）。
• 精细化的秩： 为了便于证明，作者引入了两个辅助秩：$\text{rank}_R$（层级深度）和 $\text{rank}_T$（主干深度），它们与标准秩 $\text{rank}(x)$ 密切相关。至关重要的是，他们建立了 $\text{rank}_R(\Gamma) \le \text{rank}(\Gamma) \le \omega \cdot \text{rank}_R(\Gamma)$ 的关系。这使得他们能够专注于计算 $\text{rank}_R$，因为 $\text{rank}_R$ 在 MSO 可定义性的语境下表现得更加稳健。
• 二分博弈 ($G^N_A$)： 该方法的核心是构造一个在自动机状态空间上进行的双人博弈 $G^N_A$。该博弈由一个自然数 $N$（或 $\infty$）进行参数化。
  • 玩家： $\exists$（Eloise）试图构造一个需要高秩见证的树，而 $\forall$（Abelard）试图证明低秩见证已足够。
  • 机制： 博弈涉及选择转移、方向和“选择器”（selectors），用以追踪“梳状结构”（combs，代表高秩的结构）潜在的嵌套情况。博弈通过追踪两个侧面——R（reach，到达）和 T（trunk，主干）——来模拟定义序数秩时使用的导数过程。
  • 获胜条件： 获胜条件是 $\omega$-正则的。如果 $\exists$ 能迫使路径至少发生 $N$ 次从 R 到 T 的侧面切换（对于有限的 $N$），或者在 $N=\infty$ 时发生无限次切换，或者博弈包含分支不足的拒绝路径，则 $\exists$ 获胜。若 $\forall$ 能阻止这些情况，则 $\forall$ 获胜。
• 策略分析： 作者证明了该博弈是确定的（根据 Büchi-Landweber 定理），并且在 $G^\infty_A$ 中 $\exists$ 存在必胜策略对应于 $\text{rank}_R(\Gamma) = \omega_1$，而 $\forall$ 的必胜策略则意味着 $\text{rank}_R(\Gamma) < \omega$。

3. 核心贡献与结果

主要二分定理 (Theorem 1.1)：
对于任何满足 $X$ 为良基的 MSO 公式 $\exists X. \varphi(\vec{Y}, X)$，其序数 $\text{rank}(\varphi)$ 满足严格的二分关系：

1. 严格较小： $\text{rank}(\varphi) < \omega^2$。在这种情况下，存在一个可计算的自然数 $N$，使得 $\text{rank}(\varphi) < \omega \cdot N$。
2. 极大： $\text{rank}(\varphi) = \omega_1$。

此外，对于给定的公式，判定属于哪种情况是可判定的。

可定义性结果 (第 9 节)：
论文研究了性质“$\text{rank}(X) \le \eta$”是否可以用 MSO 表示。

• 对于 $\eta < \omega$，秩 $\le \eta$ 的树语言是正规的（即 MSO 可定义的）。
• 对于 $\eta \ge \omega$，该语言不是正规的。因此，对于 $\eta \ge \omega$，谓词 $\text{rank}(X) \le \eta$ 无法直接用 MSO 表示。
• 然而，二分定理意味着，虽然 MSO 无法定义特定的巨大秩，但它可以隐式地判定秩是否受限于 $\omega^2$ 或是无界的（达到 $\omega_1$）。

在 $\mu$-演算中的应用 (第 10 节)：
作者将研究结果应用于 $\mu$-演算中不动点公式的闭包序数。

• 他们回应了 Czarnecki 提出的问题：是否存在一个 $\mu$-演算公式具有可数且 $\ge \omega^2$ 的闭包序数。
• 通过将 $\mu$-演算归约为二叉树上的 MSO，他们证明了对于向量不动点（即变量不在其他不动点算子作用范围内），其闭包序数要么 $< \omega^2$，要么 $\ge \omega_1$。
• 这为 Afshari, Barlucchi, 和 Leigh 最近建立的结果提供了一个替代证明和判定程序，并增加了可判定性以及对任意（而非仅限可数）模型的适用性。

4. 意义与主张

论文声称其主要贡献是为 MSO 中良基见证的序数秩建立了一个可判定的二分关系。

• 理论影响： 它解决了哪些序数可以作为 MSO 中的闭包序数的问题，表明其谱系是“有间隙的”：不存在介于 $\omega^2$ 和 $\omega_1$ 之间的序数。可实现的秩集合为 $\{ \alpha \mid \alpha < \omega^2 \} \cup \{ \omega_1 \}$。
• 可判定性： 不同于许多 MSO 扩展问题，作者展示了判定秩是否小于 $\omega^2$ 是可判定的。
• $\text{rank}_R$ 的稳健性： 论文强调，“层级深度”秩 ($\text{rank}_R$) 比标准秩更适合 MSO 定义性，因为它允许精确计算直到 $\omega$ 的值，而标准秩在更早阶段就会变得不可定义。
• 局限性： 作者谦虚地指出，虽然他们可以判定秩是否 $< \omega^2$ 或 $= \omega_1$，但对于标准秩而言，计算其精确值（如果其 $< \omega^2$）仍然是一个开放问题，尽管对于 $\text{rank}_R$ 是可计算的。他们还澄清，他们对 $\mu$-演算的结果适用于特定片段（变量不在不动点算子作用范围内），由于不动点迭代中固有的单调性约束，该结果并不能直接推广到一般的 MSO 领域。

总之，论文表明，虽然 MSO 无法显式定义任意大的序数秩，但它拥有足够的隐式能力来区分“小”秩（受限于 $\omega^2$）和“极大”秩（达到 $\omega_1$），而这种区别是有效可判定的。