2026-07-21T10:22:27Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6576 2025-05-14T15:26:13Z ddc:004 open_access

The Logical Strength of Büchi's Decidability Theorem Kolodziejczyk, Leszek Aleksander Michalewski, Henryk Pradic, Cécilia Skrzypczak, Michal nondeterministic automata monadic second-order logic Büchi's theorem additive Ramsey's theorem reverse mathematics 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, less_or_equal). We prove that the following are equivalent over the weak second-order arithmetic theory RCA: 1. Büchi's complementation theorem for nondeterministic automata on infinite words, 2. the decidability of the depth-n fragment of the MSO theory of (N, less_or_equal), for each n greater than 5, 3. the induction scheme for Sigma^0_2 formulae of arithmetic. Moreover, each of (1)-(3) is equivalent to the additive version of Ramsey's Theorem for pairs, often used in proofs of (1); each of (1)-(3) implies McNaughton's determinisation theorem for automata on infinite words; and each of (1)-(3) implies the "bounded-width" version of König's Lemma, often used in proofs of McNaughton's theorem. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leszek Aleksander Kolodziejczyk and Henryk Michalewski and Cécilia Pradic and Michal Skrzypczak 2016 Is Part Of LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2016.36 urn:nbn:de:0030-drops-65765 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.36 eng https://creativecommons.org/licenses/by/3.0/legalcode