THE LOGICAL STRENGTH OF BUCHI'S DECIDABILITY THEOREM

We study the strength of axioms needed to prove various results related to automata on infinite words and Buchi'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 RCA(0): (1) the induction scheme for Sigma(0)(2) formulae of arithmetic, (2) a variant of Ramsey's Theorem for pairs restricted to so-called additive colourings, (3) Buchi'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 in finite words, as well as the "bounded-width" version of Konig's Lemma, often used in proofs of McNaughton's theorem.