The logical strength of B\"uchi's decidability theorem

TL;DR

This paper explores the logical strength of B"uchi's theorem on automata and MSO theory of natural numbers, establishing equivalences with key logical and combinatorial principles within weak second-order arithmetic.

Contribution

It proves the equivalence of several fundamental theorems and principles related to automata on infinite words and logic, within a weak arithmetic framework.

Findings

Equivalence of induction, Ramsey's theorem variant, B"uchi's theorem, and MSO decidability.

Each principle implies McNaughton's determinisation theorem.

Connections between automata theory and logical strength are established.

Abstract

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.