A Dichotomy Theorem for Ordinal Ranks in MSO

기술적 요약: MSO에서의 서수 계급에 관한 이분법 정리

1. 문제 정식화

본 논문은 무한 이진 트리 위에서의 단항 이차 논리(Monadic Second-Order, MSO)의 표현력, 특히 존재 양화사의 증거 역할을 하는 **잘-정의된 집합(well-founded sets)**의 복잡성을 조사한다.

저자들은 $\exists X. \varphi(\vec{Y}, X)$ 형태의 공식을 고려하며, 여기서 $\varphi$는 임의의 MSO 공식이다. 저자들은 $\vec{Y}$의 해석(valuation)에 대해 해당 공식이 만족될 때마다, 증거가 되는 집합 $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)$$
여기서 상한(supremum)은 공식을 만족하는 모든 $\vec{Y}$에 대해 취해지며, 하한(minimum)은 모든 증거 집합 $X$에 대해 취해진다. 가산 서수의 상한은 최대 $\omega_1$(첫 번째 비가산 서수)이므로, 문제는 다음과 같다: $\text{rank}(\varphi)$의 정확한 값은 무엇인가?

기존 연구에서는 임의의 자연수 쌍 $(k, l)$에 대해 $\text{rank}(\varphi) = \omega \cdot k + l$인 공식을 구성할 수 있음이 밝혀졌다. 그러나 다른 서수들(특히 $\omega^2$ 이상 $\omega_1$ 미만인 서수들)이 MSO 공식의 폐쇄 서수로 실현될 수 있는지 여부는 알려져 있지 않았다.

2. 방법론

저자들은 이 계급들을 특징짓기 위해 게임 이론적 접근 방식을 자동사 이론(automata theory)과 결합하여 사용한다.

• 자동사 표현: MSO 공식을 직접 다루는 대신, 저자들은 MSO와 비결정론적 패리티 트리 자동사(Rabin의 정리) 사이의 동치성을 활용한다. 저자들은 가지치기 된 자동사(pruned automaton)에 의해 인식되는 정규 관계 $\Gamma \subseteq \text{Tr}_A \times \text{WF}$ (여기서 $\text{WF}$는 잘-정의된 트리들의 집합)를 정의한다.
• 정교화된 계급(Refined Ranks): 증명을 용이하게 하기 위해, 저자들은 표준 계급 $\text{rank}(x)$와 밀접하게 연관된 두 가지 보조 계급인 $\text{rank}_R$(층위 깊이, layered depth)과 $\text{rank}_T$(중심축 깊이, trunk depth)를 도입한다. 결정적으로, 저자들은 $\text{rank}_R(\Gamma) \le \text{rank}(\Gamma) \le \omega \cdot \text{rank}_R(\Gamma)$임을 입증한다. 이를 통해 MSO 정의 가능성 맥락에서 더 견고하게 작동하는 $\text{rank}_R$을 계산하는 데 집중할 수 있다.
• 이분법 게임 ($G^N_A$): 방법론의 핵심은 자동사의 상태 공간 위에서 진행되는 두 명의 플레이어 게임 $G^N_A$의 구성이다. 이 게임은 자연수 $N$(또는 $\infty$)에 의해 매개변수화된다.
  • 플레이어: $\exists$ (Eloise)는 높은 계급의 증거를 요구하는 트리를 구축하려고 시도하며, $\forall$ (Abelard)는 더 낮은 계급의 증거로도 충분함을 보여주려 한다.
  • 메커니즘: 게임은 높은 계급을 나타내는 "빗(combs)"의 잠재적 중첩을 추적하기 위한 선택(transitions), 방향(directions), 그리고 "선택자(selectors)"를 선택하는 과정을 포함한다. 게임은 계급의 도함수 과정을 모델링하기 위해 두 측면, R(reach)과 T(trunk)를 추적한다.
  • 승리 조건: 승리 조건은 $\omega$-정규( $\omega$-regular)이다. $\exists$는 경로가 $N$번(유한한 $N$의 경우) 또는 무한히 자주( $N=\omega$인 경우) R에서 T로 측면을 바꾸도록 강제하거나, 불충분한 분기를 가진 거부 경로를 포함할 경우 승리한다. $\forall$는 이러한 조건들을 방지할 수 있다면 승리한다.
• 전략 분석: 저자들은 이 게임이 결정 가능(Büchi-Landweber 정리에 의해)함을 증명하며, $G^\infty_A$에서 $\exists$의 필승 전략의 존재는 $\text{rank}_R(\Gamma) = \omega_1$과 정확히 대응하고, $\forall$의 필승 전략은 $\text{rank}_R(\Gamma) < \omega$를 의미함을 보인다.

3. 주요 기여 및 결과

주요 이분법 정리 (정리 1.1):
잘-정의된 $X$에 대한 임의의 MSO 공식 $\exists X. \varphi(\vec{Y}, X)$에 대하여, 서수 $\text{rank}(\varphi)$는 다음과 같은 엄격한 이분법을 따른다:

1. 엄격히 작은 경우 (Strictly Small): $\text{rank}(\varphi) < \omega^2$. 이 경우, $\text{rank}(\varphi) < \omega \cdot N$을 만족하는 계산 가능한 자연수 $N$이 존재한다.
2. 최대치인 경우 (Maximal): $\text{rank}(\varphi) = \omega_1$.

또한, 주어진 공식에 대해 이 두 사례 중 어느 것이 해당하는지 결정 가능하다(decidable).

정의 가능성 결과 (섹션 9):
논문은 "$\text{rank}(X) \le \eta$"라는 성질이 MSO에서 표현 가능한지 조사한다.

• $\eta < \omega$인 경우, 계급이 $\le \eta$인 트리들의 언어는 정규(regular)이며 MSO로 정의 가능하다.
• $\eta \ge \omega$인 경우, 해당 언어는 정규가 아니다. 결과적으로, $\eta \ge \omega$에 대해 술어 $\text{rank}(X) \le \eta$는 MSO로 직접 표현될 수 없다.
• 그러나 이 이분법 정리는 MSO가 특정 큰 계급을 정의할 수는 없지만, 계급이 $\omega^2$에 의해 제한되는지 아니면 무한한지($\omega_1$에 도달하는지)를 암묵적으로 결정할 수 있음을 시사한다.

$\mu$-Calculus에 대한 적용 (섹션 10):
저자들은 자신들의 결과를 $\mu$-calculus의 고정점 공식(fixed-point formulas)의 폐쇄 서수에 적용한다.

• 저자들은 벡터 고정점(variables do not occur in the scope of other fixed-point operators)에 대해 폐쇄 서수가 $\omega^2$ 이상의 가산 서수를 가질 수 있는지에 대한 Czarnecki의 질문을 다룬다.
• $\mu$-calculus를 이진 트리 상의 MSO로 환원함으로써, 저자들은 벡터 고정점의 경우 폐쇄 서수가 $\omega^2$ 미만이거나 $\omega_1$ 이상임을 증명한다.
• 이는 Afshari, Barlucchi, Leigh가 최근 확립한 결과에 대한 대안적인 증명과 결정 절차를 제공하며, 계산 가능성과 임의의 모델에 대한 적용 가능성이라는 이점을 더한다.

4. 의의 및 주장

본 논문은 자신의 주요 기여가 잘-정의된 증거의 서수 계급에 대한 **결정 가능한 이분법(decidable dichotomy)**을 확립한 것임을 주장한다.

• 이론적 영향: 본 논문은 MSO에서 어떤 서수들이 폐쇄 서수로 나타날 수 있는지를 해결하며, 그 스펙트럼이 "간극(gap)"이 있음을 보여준다. 즉, $\omega^2$와 $\omega_1$ 사이의 서수들은 달성 불가능하다. 달성 가능한 계급의 집합은 $\{ \alpha \mid \alpha < \omega^2 \} \cup \{ \omega_1 \}$이다.
• 결정 가능성: MSO 확장 문제들의 많은 경우와 달리, 저자들은 계급이 $\omega^2$보다 작은지 여부를 판단하는 것이 결정 가능함을 보여준다.
• $\text{rank}_R$의 견고성: 논문은 "층위 깊이" 계급($\text{rank}_R$)이 표준 계급보다 MSO 정의 가능성 측면에서 더 견고한 척도임을 강조한다. 이는 표준 계급이 훨씬 일찍 정의 불가능해지는 것과 달리, $\text{rank}_R$은 $\omega$까지의 값을 정확히 계산할 수 있게 해주기 때문이다.
• 한계: 저자들은 $\text{rank}(\varphi)$가 $\omega^2$보다 작은지 혹은 $\omega_1$인지 결정할 수는 있지만, 만약 $\text{rank}(\varphi) < \omega^2$일 때 그 정확한 값을 계산하는 것은 (표준 계급에 대해) 여전히 미해결 과제로 남아 있다고 겸허히 언급한다. 또한, $\mu$-calculus에 대한 결과는 특정 파편(고정점 연산자의 범위 내에 변수가 존재하지 않는 경우)에 적용되는 것이며, 고정점 반복 과정에 내재된 단조성 제약으로 인해 일반적인 MSO 영역으로 즉시 전이되지는 않는다고 명시한다.

요약하자면, 본 논문은 MSO가 임의의 큰 서수 계급을 명시적으로 정의할 수는 없지만, "작은" 계급($\omega^2$에 의해 제한됨)과 "최대" 계급($\omega_1$)을 구별할 수 있는 충분한 암묵적 능력을 갖추고 있으며, 이 구분이 효과적으로 결정 가능하다는 것을 입증한다.