Kołodziejczyk, Leszek and Michalewski, Henryk and Pradic, Pierre and Skrzypczak, Michał - The logical strength of Büchi's decidability theorem

lmcs:4866 - Logical Methods in Computer Science, May 23, 2019, Volume 15, Issue 2 - https://doi.org/10.23638/LMCS-15(2:16)2019
The logical strength of Büchi's decidability theorem

Authors: Kołodziejczyk, Leszek and Michalewski, Henryk and Pradic, Pierre and Skrzypczak, Michał

We study the strength of axioms needed to prove various results related to automata on infinite words and Büchi'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üchi'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önig's Lemma, often used in proofs of McNaughton's theorem.


Volume: Volume 15, Issue 2
Published on: May 23, 2019
Submitted on: October 2, 2018
Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic


Share

Consultation statistics

This page has been seen 211 times.
This article's PDF has been downloaded 136 times.