Leszek Kołodziejczyk ; Henryk Michalewski ; Pierre Pradic ; Michał Skrzypczak - 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 theoremArticle

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

    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
    Accepted on: October 24, 2018
    Submitted on: October 2, 2018
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1239 times.
    This article's PDF has been downloaded 463 times.