The logical strength of Büchi's decidability theorem

We study the strength of axioms needed to prove various results related toautomata on infinite words and B ̈uchi’s theorem on the decidability of theMSOtheory of(N,≤). We prove that the following are equivalent over the weak second-order arithmetictheoryRCA0:(1) the induction scheme for Σ02formulae of arithmetic,(2) a variant of Ramsey’s Theorem for pairs restricted to so-calledadditive colourings,(3) B ̈uchi’s complementation theorem for nondeterministic automata on infinite words,(4)the decidability of the depth-nfragment of theMSOtheory of (N,≤), for eachn≥5,Moreover, each of (1)–(4) implies McNaughton’s determinisation theorem for automataon infinite words, as well as the “bounded-width” version of K ̈onig’s Lemma, often used inproofs of McNaughton’s theorem.