| Summary: | 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 $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) 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 $n \ge 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\"onig's
Lemma, often used in proofs of McNaughton's theorem.
|
|---|