The Logical Strength of Büchi's Decidability Theorem.

We study the strength of axioms needed to prove various results related to automata on infinite words and Buchiu0027s 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. Buchiu0027s 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 Ramseyu0027s Theorem for pairs, often used in proofs of (1); each of (1)-(3) implies McNaughtonu0027s determinisation theorem for automata on infinite words; and each of (1)-(3) implies the bounded-width version of Konigu0027s Lemma, often used in proofs of McNaughtonu0027s theorem.