The logical strength of B\"uchi's decidability theorem

MaRDI QIDQ6276899arXivFDO

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

Publication date 26 August 2016

Published in arXiv

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Automata and formal grammars in connection with logical questions (03D05) Second- and higher-order arithmetic and fragments (03F35)

arXiv classification

cs.LOmath.LO

Abstract: We study the strength of axioms needed to prove various results related to automata on infinite words and B"uchi'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 $RC{A}_0$: (1) the induction scheme for $Sigm{a}_2^0$ formulae of arithmetic, (2) a variant of Ramsey's Theorem for pairs restricted to so-called additive colourings, (3) B"uchi'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 $nge5$. Moreover, each of (1)-(4) implies McNaughton's determinisation theorem for automata on infinite words, as well as the "bounded-width" version of K"onig's Lemma, often used in proofs of McNaughton's theorem.

This page was built for publication: The logical strength of B\"uchi's decidability theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6276899)