一句话：在 RCA0 上证明 Büchi 可判定性相关定理与 Σ^0_2 归纳、加性 Ramsey 定理等价，并蕴含 McNaughton 确定化。
论文研究无限字自动机与 Büchi 关于 (N,≤) 的 MSO 理论可判定性所需公理的逻辑强度。作者在弱二阶算术 RCA0 中证明以下命题等价：(1) 算术 Σ^0_2 公式的归纳模式；(2) 限定于加性着色的二元 Ramsey 定理变体；(3) 非确定无限字自动机的 Büchi 补余定理；(4) 对每个 n≥5，(N,≤) 的 MSO 理论深度 n 片段可判定。并进一步证明这些命题均蕴含无限字自动机的 McNaughton 确定化定理，以及证明该定理常用的“有界宽度”König 引理。该结果以逆向数学方式厘清了 Büchi 可判定性定理及相关自动机结果的逻辑强度，将其与算术归纳和 Ramsey 型组合原理联系起来。
We study the strength of axioms needed to prove various results related to automata on infinite words and B\"uchi's theorem on the decidability of the MSO theory of $(N, {\le})$. We prove that the following are equivalent over the weak second-order arithmetic theory $RCA_0$: (1) the induction scheme for $\Sigma^0_2$ formulae of arithmetic, (2) a variant of Ramsey's Theorem for pairs restricted to so-called additive colourings, (3) B\"uchi's complementation theorem for nondeterministic automata on infinite words, (4) the decidability of the depth-$n$ fragment of the MSO theory of $(N, {\le})$, for each $n \ge 5$. Moreover, each of (1)-(4) implies McNaughton's determinisation theorem for automata on infinite words, as well as the "bounded-width" version of K\"onig's Lemma, often used in proofs of McNaughton's theorem.
@article{paperbot792,
title = {The logical strength of B\"uchi's decidability theorem},
author = {Leszek Kołodziejczyk and Henryk Michalewski and Cécilia Pradic and Michał Skrzypczak},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 2},
year = {2019},
doi = {10.23638/lmcs-15(2:16)2019}
}