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,). We prove that the following are equivalent over the weak second-order arithmetic theory RCA0: (1) the induction scheme for Σ02 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,), for each n5. 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 2287 times.
    This article's PDF has been downloaded 576 times.