![]() |
![]() |
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 n≥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.