The logical strength of Büchi's decidability theorem
The logical strength of Büchi's decidability theorem
复制标题
Büchi 可判定性定理的逻辑强度
DOI：
10.23638/lmcs-15(2:16)2019
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Michal Skrzypczak
中科院分区：
文献类型：
--
作者：
L. Kolodziejczyk;H. Michalewski;Cécilia Pradic;Michal Skrzypczak
我们研究的强度公理需要证明各种结果的自动机上无限的话和布奇定理的MSO理论的可判定性$（N，{\le}）$。我们证明了在弱二阶算术理论RCA_0 $上下列是等价的：
(1)算术公式的归纳法，
(2)Ramsey定理的一个变体，用于限制于所谓的加性着色的对，
(3)无限词上不确定自动机的Buchi互补定理，
(4)的可判定性的深度$n$片段的MSO理论的$（N，{\le}）$，对于每个$n \ge 5$。
此外，（1）-（4）中的每一个都包含了无限词上自动机的麦克诺顿决定定理，以及柯尼希引理的“有界宽度”版本，经常用于麦克诺顿定理的证明。
We study the strength of axioms needed to prove various results related to automata on infinite words and Buchi'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) Buchi'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 Konig's Lemma, often used in proofs of McNaughton's theorem.