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 theory of $(\Nn, {\le})$. We prove that the following are equivalent over the weak second-order arithmetic theory $\rca$:

* Büchi's complementation theorem for nondeterministic automata on infinite words,

* the decidability of the depth-$n$ fragment of the theory of $(\Nn, {\le})$, for each $n \ge 5$,

* the induction scheme for $\Sigma^0_2$ formulae of arithmetic.

Moreover, each of (1)-(3) is equivalent to the additive version of Ramsey's Theorem for pairs, often used in proofs of (1); each of (1)-(3) implies McNaughton's determinisation theorem for automata on infinite words; and each of (1)-(3) implies the “bounded-width” version of König's Lemma, often used in proofs of McNaughton's theorem.

§ INTRODUCTION

Büchi's theorem [3] states that the monadic second-order theory of $(\Nn, {\le})$ is decidable. This is one of the  fundamental results on the decidability of logical theories, and no less fundamental are the methods developed in order to prove it.

Typical proofs of Büchi's theorem  make use of automata on infinite words. Büchi's original argument involved obtaining a complementation theorem for nondeterministic word automata: for each such automaton $\Aa$, there is another automaton $\Bb$ which accepts a given word exactly if $\Aa$ does not. Thanks to the complementation theorem, an formula can be inductively translated into an equivalent nondeterministic automaton. At that point, checking satisfiability of the formula becomes a matter of elementary combinatorics. Another approach to decidability of was presented by Shelah in [17]. Shelah's “composition method” is automata-free, but is similar to Büchi's proof in one important respect: both use a restricted form of Ramsey's Theorem.

McNaughton [13] showed that an infinite word automaton can be determinised, though at the cost of allowing automata with a more general acceptance condition than Büchi's.
Since deterministic automata are easy to complement, this again gives the translation of formulae to automata and thus decidability of . To the best of our knowledge all determinisation proofs known from the literature rely on  either a restricted form of Ramsey's Theorem or a restricted form of König's Lemma.

It is natural to ask how the various proofs of Büchi's theorem and related results compare to one another. For instance, is determinisation of word automata an “essentially stronger” result than complementation? Also, is the use of mildly nonconstructive principles à la Ramsey or König unavoidable?

A convenient framework for studying questions of this sort is provided by the programme of reverse mathematics [18]. The idea is to compare various theorems as formalised in the very expressive language of an axiomatic theory known as second-order arithmetic. Typical subtheories of second-order arithmetic are axiomatised by principles asserting the existence of more or less complicated sets of natural numbers. An important example is the relatively weak theory $\rca$, which guarantees only the existence of decidable sets. $\rca$ can formalise a significant amount of everyday mathematics and prove the termination of any primitive recursive algorithm, but it is unable to prove the existence of noncomputable objects such as the homogeneous sets postulated by Ramsey's Theorem or the infinite branches postulated by König's Lemma. Sometimes it is possible to show that two theorems not provable in $\rca$ are provably equivalent in it, and thus neither theorem is logically stronger than the other in the sense of requiring more abstract or less constructive sets. It is also often the case that a set existence principle used to derive some theorem is actually implied by the theorem over $\rca$.
This serves as evidence that the principle is in fact necessary to prove the theorem.

In this paper, we carry out a reverse-mathematical study of the results around Büchi's theorem.
We have two main aims in mind. One is to compare complementation, determinisation and decidability of MSO in terms of logical strength. The other aim is to clarify the role of Ramsey's Theorem and König's Lemma in proofs of Büchi's theorem and the related facts about automata. This seems interesting in light of the fact that the usual formulation of Ramsey's Theorem for pairs and the so-called Weak König's Lemma (the form of König's Lemma most commonly needed in practice) are known to be incomparable over $\rca$ [7, 12].

Our findings are as follows: firstly, determinisation of infinite word automata is no stronger than complementation, at least in the sense of implication over $\rca$. Secondly, decidability of over $(\Nn,{\le})$ implies both complementation and determinisation.
Finally, the use of Ramsey- or König-like principles in proofs of Büchi's theorem is mostly spurious in the sense that the versions that are actually needed follow from a very limited set-existence principle, namely mathematical induction for properties expressed by $\Sigma^0_2$ formulae. More precisely, we prove:

Over $\rca$, the following statements are equivalent:

* the principle of mathematical induction for the formulae in $\Sigma^0_2$ (denoted $\Sigma^0_2\ind$),

* the Additive Ramsey Theorem (see Definition <ref>),

* complementation for Büchi automata: there exists an algorithm which for each nondeterministic Büchi automaton $\Aa$ outputs a Büchi automaton $\Bb$ such that for every infinite word $\infA$, $\Bb$ accepts $\infA$ exactly if $\Aa$ does not accept $\infA$,

* the decidability of the depth-$n$ fragment of the $\mso$ theory of $(\Nn, {\le})$ (where $n \geq 5$ is a natural number)[The restriction to fixed-depth fragments is a technicality related to undefinability of truth. This is explained in more detail in Section <ref>.].

Furthermore, each of <ref>.–<ref>. implies:

* determinisation of Büchi automata: there exists an algorithm which for each nondeterministic Büchi automaton $\Aa$
outputs a deterministic Rabin automaton $\Bb$ such that for every infinite word $\infA$, $\Bb$ accepts $\infA$ exactly if $\Aa$ accepts $\infA$.

We also give a precise statement of the bounded-width form of König's Lemma often used in proofs of Item <ref>., and show that it is implied by each of <ref>.–<ref>. Interestingly, it is not clear if <ref>. implies <ref>.–<ref>. over $\rca$: standard arguments used to complement deterministic automata with acceptance conditions other than Büchi seem to involve $\Sigma^0_2\ind$.

It follows from our results that Büchi's theorem is unprovable in $\rca$, but only barely: it is true in computable mathematics, in the sense that the theorem remains valid if all the set quantifiers are restricted to range over (exactly) the decidable subsets of $\Nn$. This is in stark contrast to the behaviour of Rabin's theorem on the decidability of on the infinite binary tree, which is known to require the existence of extremely complicated noncomputable sets [10]. Also Additive Ramsey's Theorem and Bounded-width König's Lemma are true in computable mathematics—quite unlike more general forms of Ramsey's Theorem for pairs and König's Lemma [8, 11].

To prove the implication $(\ref{it:dec_mso} \to \ref{it:induction})$ of Theorem <ref>, we come up with a family of sentences for which truth in $(\Nn,{\le})$ is undecidable if $\Sigma^0_2\ind$ fails. The other implications are proved by formalising more or less standard arguments from automata theory. In some cases this is routine, but especially the proof of $(\ref{it:induction}\to \ref{it:det_buchi})$ is quite delicate: we have to check not only that $\Sigma^0_2\ind$ implies Bounded-width König's Lemma, but also that constructing the objects to which we apply the lemma is within the means of $\rca + \Sigma^0_2\ind$.

The structure of the paper is as follows.
Sections <ref> and <ref> discuss the necessary background on reverse mathematics, automata, and .
We prove
$(\ref{it:induction}\to \ref{it:ramsey})$    in Section <ref>,
$(\ref{it:ramsey}\to \ref{it:compl_buchi})$  in Section <ref>,
$(\ref{it:compl_buchi}\to \ref{it:dec_mso})$ in Section <ref>,
$(\ref{it:dec_mso} \to \ref{it:induction})$  in Section <ref>.
Section <ref> contains a proof that $\Sigma^0_2\ind$ implies Bounded-width König's Lemma, which is then applied to prove
$(\ref{it:induction}\to \ref{it:det_buchi})$ in Section <ref>.

§ BACKGROUND ON REVERSE MATHEMATICS

Reverse mathematics [18] is a framework for studying the strength of axioms needed to prove theorems of countable mathematics, that is, the part of mathematics concerned with objects that can be represented using no more than countably many bits of information. This encompasses the vast majority of the mathematics needed in computer science.

The basic idea of reverse mathematics is to analyse mathematical theorems in terms of subsystems of a strong axiomatic theory known as second-order arithmetic. The two-sorted language of second-order arithmetic, $L_2$, contains first-order variables $x, y, z, \ldots$ (or $i,j,k,\ldots$), intended to range over natural numbers, and second-order variables $X,Y,Z,\ldots$, intended to range over sets of natural numbers. $L_2$ includes the usual arithmetic functions and relations ${+}, {\cdot}, {\le}, 0,1$ on the first-order sort, and the ${\in}$ relation which has one first-order and one second-order argument.
The intended model of $\mathsf{Z}_2$ is $(\omega, \mathcal{P}(\omega))$.

Notational convention.
From this point onwards, we will use the letter $\Nn$ to denote the natural numbers as formalised in second-order arithmetic, that is, the domain of the first-order sort. On the other hand, the symbol $\omega$ will stand for the concrete, or standard, natural numbers. For instance, given a theory $\mathrm{T}$ and a formula $\varphi(x)$, “$\mathrm{T}$ proves $\varphi(n)$ for all $n \! \in \! \omega$” will mean “$\mathrm{T} \vdash \varphi(0), \mathrm{T} \vdash \varphi(1), \ldots$”, which does not have to imply $\mathrm{T} \vdash \forall x\!\in\!\Nn.\, \varphi(x)$.

Full second-order arithmetic, $\mathsf{Z}_2$, has axioms of three types: (i) axioms stating that the first-order sort is the non-negative part of a discretely ordered ring; (ii) comprehension axioms, or sentences of the form
\[\forall \bar Y \, \forall \bar y\, \exists X\, \forall x\, \big(x\in X \Leftrightarrow \varphi(x, \bar Y, \bar y)\big),\]
where $\varphi$ is an arbitrary formula of $L_2$ not containing the variable $X$; (iii) the induction axiom,

\[\forall X\, \big[0 \in X \land \forall x\, (x \in X \Rightarrow x+1 \in X)\Rightarrow \forall x.\ x\in X \big].\]

The language $L_2$ is very expressive, as the first-order sort can be used to encode arbitrary finite objects and the second-order sort can encode even such objects as complete separable metric spaces, continuous functions between them, and Borel sets within them (cf. <cit.>). Moreover, the theory $\mathsf{Z}_2$ is powerful enough to prove almost all theorems from a typical undergraduate course that are expressible in $L_2$. In fact, the basic observation underlying reverse mathematics [18] is that many important theorems are equivalent to various fragments of $\mathsf{Z}_2$, where the equivalence is proved in some specific weaker fragment, referred to as the base theory.

Quantifier hierarchies.
Typical fragments of $\mathsf{Z}_2$ are defined in terms of well-known quantifier hierarchies whose definitions we now recall. A formula is $\Sigma^0_n$ if it has the form $\exists \bar{x}_1\, \forall\bar{x}_2\, \ldots\, \mathsf{Q}\bar{x}_n.\ \psi$, where the $\bar x_i$'s are blocks of first-order variables, the shape of $\mathsf{Q}$ depends on the parity of $n$, and $\psi$ is $\Delta^0_0$, i.e. contains only bounded first-order quantifiers. A formula is $\Pi^0_n$ if it is the negation of a $\Sigma^0_n$ formula. A formula is arithmetical if it contains only first-order quantifiers (second-order parameters are allowed).

A formula is $\Sigma^1_n$ if it has the form $\exists \bar{X}_1\, \forall\bar{X}_2\, \ldots \mathsf{Q}\bar{X}_n. \ \psi$, where the $\bar X_i$'s are blocks of first-order variables, the shape of $\mathsf{Q}$ depends on the parity of $n$, and $\psi$ is arithmetical. A formula is $\Pi^1_n$ if it is the negation of a $\Sigma^1_n$ formula.

In practice, we say that a formula is $\Sigma^i_n/\Pi^i_n$ if it  equivalent to a $\Sigma^i_n/\Pi^i_n$ formula
in the axiomatic theory we are working in at a given point.

Definition of $\rca$.
The usual base theory in reverse mathematics is $\rca$, which guarantees only the existence of decidable sets. $\rca$ is defined by restricting the comprehension scheme to $\Delta^0_1$-comprehension, which takes the form:

\[\forall \bar Y \, \forall \bar y\, \left[\forall x\, (\varphi(x,\bar Y, \bar y) \Leftrightarrow \neg\psi(x,\bar Y, \bar y)) \Rightarrow \exists X\, \forall x\, (x\in X \Leftrightarrow \varphi(x, \bar Y, \bar y)) \right],\]

where both $\varphi$ and $\psi$ are $\Sigma^0_1$. For technical reasons, it is necessary to strengthen the induction axiom to $\Sigma^0_1\ind$, that is, the scheme $\Sigma^0_1\ind$ consisting of the sentences

\[\forall \bar Y \, \forall \bar y\, \left[\varphi(0,\bar Y, \bar y) \land \forall x\, \left(\varphi(x,\bar Y, \bar y) \Rightarrow \varphi(x+1,\bar Y, \bar y)\right)
\Rightarrow \forall x.\ \varphi(x,\bar Y, \bar y) \right]\]

for $\varphi$ in $\Sigma^0_1$.  $\Sigma^0_1\ind$ makes it possible to define sequences by primitive recursion (cf. <cit.>): given some $x_0$ and a function $\fun{f}{\Nn}{\Nn}$, $\rca$ proves that there is a unique sequence $(x_i)_{i \in \Nn}$ such that $x_{i+1}=f(x_i)$ for each $i$.

$\rca$ has a unique minimal model in the sense of embeddability. This minimal model is $(\omega, \mathrm{Dec})$, where $\mathrm{Dec}$ is the family of decidable subsets of $\omega$.

The $\Sigma^0_n\ind$ scheme.

In this paper we study an extension of $\rca$ obtained by strengthening the induction scheme to $\Sigma^0_2$ formulae. In general,
for $n \! \in \! \omega$, the axiom scheme $\Sigma^0_n\ind$ is defined just like $\Sigma^0_1\ind$, but with the induction formula $\varphi$ in $\Sigma^0_n$ rather than $\Sigma^0_1$.  For each $n$, $\rca + \Sigma^0_n\ind$ is equivalent to $\rca + \Pi^0_n\ind$, where the latter is defined in the natural way, as well as to the least number principle for $\Sigma^0_n$ or $\Pi^0_n$ formulae (cf. <cit.>).

Two important principles provable from $\Sigma^0_n\ind$ are $\Sigma^0_n$-collection:

\[\forall \bar Z \, \forall \bar z\,
\big[\forall x \! \le \! t \,\exists y. \ \varphi(x,y,\bar Z, \bar z)\big]
\Rightarrow \exists w\, \forall x \! \le \! t \, \exists y \! \le \! w.\ \varphi(x,y,\bar Z, \bar z),\]

for $\varphi$ in $\Sigma^0_n$, and bounded $\Sigma^0_n$-comprehension:

\[\forall \bar Y \, \forall \bar y\, \forall w \, \exists X\, \forall x\, (x\in X \Leftrightarrow x \le w \land \varphi(x, \bar Y, \bar y)),\]

for $\varphi$ in $\Sigma^0_n$.

For each $n$, the theory $\rca + \Sigma^0_{n+1}\ind$ is strictly stronger than $\rca + \Sigma^0_{n}\ind$ (cf. e.g. <cit.>).
However, note that the minimal model $(\omega, \mathrm{Dec})$ of $\rca$ satisfies $\rca + \Sigma^0_n\ind$ for all $n$, because an induction axiom is always true in a model with first-order universe $\omega$.

Additive Ramsey's Theorem; Bounded-width König's Lemma.

Two prominent extensions of $\rca$ are related to weak forms of important nonconstructive set existence principles: König's Lemma and Ramsey's Theorem.

Weak König's Lemma is the statement: “for every $k$, every infinite tree contained in
$\{0,1,\ldots,k\}^\ast$ has an infinite branch”.
The theory obtained by adding this statement to $\rca$ is known as $\wkl$. This is the minimal theory supporting all sorts of “compactness arguments” in combinatorics, topology, analysis, and elsewhere (cf. <cit.>).

The theory $\rt^2_2$ extends $\rca$ by an axiom expressing Ramsey's Theorem for pairs and two colours[By $[X]^2$ we denote the set of unordered pairs of elements of $X$.]: for every $2$-colouring of $[\Nn]^2$ there exists an infinite homogeneous set. $\rt^2_{<\infty}$ is defined similarly but allowing $k$-colourings for each $k \! \in \! \Nn$.

Both $\rt^2_2$ and $\rt^2_{<\infty}$ are known to be incomparable with $\wkl$ in the sense of implication over $\rca$ [7, 12].
$\wkl$, $\rt^2_2$, and $\rt^2_\infty$ are all false in the minimal model $(\omega, \mathrm{Dec})$ of $\rca$ [8, 11]. Much more on these theories can be found in [6].

In this paper, we study specific restricted versions of $\wkl$ and $\rt^2_{<\infty}$ which play a role in proofs of Büchi's theorem.
Recall that a semigroup is a set $S$ with an associative operation $\fun{{*}}{S\times S}{S}$.

The Additive Ramsey Theorem is the following statement: for every finite semigroup $(S, {*})$ and every colouring $\fun{\colA}{[\Nn]^2}{S}$ such that for every $i \! < \! j \! < \! k$ we have $\colA(i,j) * \colA(j, k) = \colA(i, k)$, there exists an infinite homogeneous set $I \subseteq \Nn$. That is, there is a fixed color $a$ such that for every $(i, j) \in [I]^2$, $\colA(i, j) = a$.

Bounded-width König's Lemma is the following statement: for every finite set $Q$ and every graph $G$ whose vertices belong to $Q\times\Nn$ and whose edges are all of the form $((q,i),(q',i+1))$ for some $q,q'\!\in\!Q$, if there are arbitrarily long finite paths in $G$ starting in some vertex $(q,0)$, then there is an infinite path in $G$ starting in $(q,0)$.

Notice that Bounded-width König's Lemma applied to a graph $G$ is essentially the same as Weak König's Lemma applied to the tree obtained by the so-called unraveling of $G$ (in particular, Bounded-width König's Lemma is provable in $\wkl$). However, the graph formulation is more natural to express.

§ BACKGROUND ON MSO AND BÜCHI AUTOMATA

Büchi automata and logic are equivalent formalisms for specifying properties of infinite words. In this section we formally introduce these concepts. If not stated otherwise, the formalisation presented here is carried out in $\rca$.

Infinite words

By $\Sigma$ we denote a finite nonempty set  called an alphabet. A finite word over $\Sigma$ is a function $\fun{w}{\{0,\ldots,k-1\}}{\Sigma}$; the length of $w$ is $k$. The set of all finite words over $\Sigma$ is denoted $\Sigma^\ast$. An infinite word over $\Sigma$ is a function $\fun{\infA}{\Nn}{\Sigma}$. We write $\alpha \in \Sigma^\Nn$ for “$\alpha$ is an infinite word over $\Sigma$”.

Every infinite word can be treated as a relational structure with the universe $\Nn$ and predicates: the binary order predicate ${\leq}$ and a unary predicate $a$ for every $a\in \Sigma$. The semantics of these predicates over a given infinite word $\infA$ is natural, in particular $a(x)$ holds if $\infA(x)=a$.

When working with automata and logic it is natural to consider languages—sets of infinite words satisfying certain properties. However, from the point of view of second-order arithmetic a language is a “third-order object”. Therefore, in this paper we avoid talking directly about languages. Instead, when we want to express some properties of languages, we explicitly quantify over infinite words with a given property.

Automata over infinite words

A (nondeterministic) Büchi automaton is a tuple $\Aa=\langle Q, \Sigma, q_\init, \delta, F\rangle$ where: $Q$ is a finite set of states, $\Sigma$ is an alphabet, $q_\init\in Q$ is an initial state, $\delta\subseteq Q\times \Sigma\times Q$ is the transition relation, and $F\subseteq Q$ is the set of accepting states. Given an infinite word $\infA\in \Sigma^\Nn$, we say that $\rho\in Q^\Nn$ is a run of $\Aa$ over $\infA$ if $\rho(0)= q_\init$ and for every $n\in\Nn$ we have $\big(\rho(n),\infA(n),\rho(n+1)\big)\in\delta$. A run $\rho$ is accepting if $\rho(n)\in F$ for infinitely many $n\in\Nn$. An automaton $\Aa$ accepts $\infA$ if there exists an accepting run of $\Aa$ over $\infA$. An automaton is deterministic if for every $q\in Q$ and $a\in\Sigma$ there is at most one transition of the form $(q,a,q') \in \delta$. When the automaton is not clear from the context, we put it in the superscript, i.e. $Q^\Aa$ is the set of states of $\Aa$.

The possible transitions of a Büchi automaton over a particular letter $a\in\Sigma$ can be encoded as a transition matrix $\fun{M_a}{Q\times Q}{\{\trNon,\trYes,\trAcc\}}$, where $M_a(q,q')=\trNon$ if $(q,a,q')\notin\delta$, otherwise $M_a(q,q')=\trAcc$ if $q\in F$, and otherwise $M_a(q,q')=\trYes$. Let $[Q]$ be the set of all such functions $\fun{M}{Q\times Q}{\{\trNon,\trYes,\trAcc\}}$.

Since deterministic Büchi automata are strictly weaker than general Büchi automata [15], one introduces the more flexible Rabin acceptance condition in order to determinise Büchi automata. A Rabin automaton is a tuple $\Aa=\langle Q, \Sigma, q_\init, \delta, (E_i, F_i)_{i=1}^k \rangle$ as in the case of Büchi automata, where $E_i,F_i\subseteq Q$ for $i=1,\ldots,k$. A run $\rho \in Q^\Nn$ of $\Aa$ is accepting if and only if for some $i\in\{1,\ldots,k\}$ each state in $E_i$ appears only finitely many times in $\rho$ and some state in $F_i$ appears infinitely many times in $\rho$.

In general (i.e. in $\mathsf{Z}_2$) Rabin automata can easily be complemented into so-called Streett automata, and both classes can be transformed into nondeterministic Büchi automata. However, the transformations into Büchi automata require more than $\rca$. For Streett automata, $\Sigma^0_2\ind$ seems necessary. For Rabin, we need the Büchi automaton to guess that no state from a given set of states will reappear in the run under consideration. To prove that such a construction is correct one needs $\Sigma^0_2$-collection—within $\rca$ the fact that in a given run $\rho$ each state $q\in E$ appears only finitely many times does not imply a global bound after which no state from $E$ reappears. That is the essential reason why it is not clear whether Item <ref>. of Theorem <ref> implies the other items
in $\rca$.

Monadic Second-Order logic

Monadic second-order logic () is an extension of first-order logic.

logic allows: boolean connectives ${\lnot}$, ${\lor}$, ${\land}$; the first-order quantifiers $\exists x$ and $\forall x$; and the monadic second-order quantifiers $\exists X$ and $\forall X$, where the variable $X$ ranges over subsets of the universe. Apart from  predicates from the signature of a given structure, the logic admits the binary predicate $x\in X$ with the natural semantics.

Definition of truth for $\mso$ over $\Nn$

In order to state our theorems involving decidability of the $\mso$ theory
of $(\Nn,{\le})$, we need to formulate the semantics of  monadic second-order logic within $\rca$. This involves a coding of formulae $\phi \mapsto \godelize{\phi}$; we identify a formula with its code. However, in second-order arithmetic there is no canonical definition of truth in an infinite structure which would work for all of . Moreover, by Tarski's theorem on the undefinability of truth, for some infinite structures there is no such definition at all. In particular, it is not at all clear how to state the decidability of  $\mso(\Nn,{\le})$ as a single sentence.

On the other hand, already $\rca$ is able to express a truth definition for the depth-$n$ fragment of $\mso$, for each $n \in \omega$. Here the depth of a formula is calculated as the largest number of alternating blocks of $\land$/$\forall$'s and $\lor$/$\exists$'s appearing on a branch in the syntactic tree of the formula (assume that all negations are pushed inside using the De Morgan laws). Essentially, the truth definition needs
one universal set quantifier for a block of $\land$/$\forall$'s and
one existential set quantifier for a block of $\lor$/$\exists$'s[After slight modifications, the truth definition would still work if we allowed depth-$n$ formulas to contain arbitrarily many alternations $\land$'s and $\lor$'s inside the scope of the last quantifier counted towards the depth.].

So, what is possible is to provide formulae $\varphi_n$ stating that the depth-$n$ fragment of $\mso(\Nn,{\le})$ is decidable. We show in Section <ref> that every $\varphi_n$ can be proved in $\rca$ assuming a complementation procedure for Büchi automata, and in Section <ref> that $\varphi_5$ implies $\Sigma^0_2\ind$. As a corollary, we can observe that $\rca \vdash \varphi_5 \Rightarrow \varphi_n$ for every $n \in \omega$.

The Büchi decidability theorem

In [3] Büchi proved decidability of the theory $\mso(\Nn,{\le})$. The following theorem captures as much of Büchi's result as can be naturally expressed in relatively weak theories of second-order arithmetic.

There exists an effective procedure $P$ such that for every fixed depth $n\!\in \!\omega$ the following is provable in $\rca+\Sigma^0_2\ind$. For every statement $\phi$ of over an alphabet $\Sigma$ such that the depth of $\phi$ is at most $n$, the procedure $P(\phi)$ produces a nondeterministic Büchi automaton $\Aa$ over $\Sigma$ such that for every infinite word $\infA\!\in\!\Sigma^\Nn$, this word satisfies $\phi$ if and only if $\Aa$ accepts $\infA$. Moreover, it is decidable if a given nondeterministic Büchi automaton accepts any infinite word.

We discuss some issues related to formalising the inductive proof of Büchi's theorem in Section <ref>. The crucial step concerns complementation of automata, which is used to treat negations of subformulae in $\phi$ (or subformulae beginning with $\forall$, assuming the negations have been pushed inside).

§ IND IMPLIES ADDITIVE RAMSEY

The aim of this section is to prove the following theorem.

The proof consists of two steps. First, we prove another weakening of Ramsey's Theorem.

Ordered Ramsey's Theorem for pairs states that if $(P, \preceq)$ is a finite partial order and $\fun{\colA}{[\Nn]^2}{P}$ is a colouring such that for every $i\! <\! j\! <\! k$ we have $\colA(i, j) \succeq \colA(i, k)$, then there exists an infinite homogeneous set $I\subseteq \Nn$, i.e. $\colA(i,j)=\colA(i',j')$ for all $(i,j),(i',j')\in [I]^2$.

Note that this statement follows immediately from the so-called  Stable Ramsey's Theorem $\srt^2_{<\infty}$ (cf. <cit.>), where the requirement on $\colA$ is only that $\colA(i,\cdot)$ should stabilise for each $i$.

Over $\rca$, $\Sigma^0_2\ind$ proves Ordered Ramsey's Theorem.

We call a colour $p\in P$ recurring if $\forall i\, \exists k\!>\!j\!>\!i.\ \colA(j,k)=p$. Notice that for each non-recurring colour $p$ there exists $i_p$ such that there is no occurrence of $p$ to the right of $i_p$ (i.e. no $k>j>i_p$ such that $\colA(j,k)=p$). By an application of $\Sigma^0_2$-collection we obtain some $i_0$ such that for every non-recurring colour $p$ and every $k>j>i_0$ we have $\colA(j,k)\neq p$. In particular, there is a recurring colour. Moreover, being a recurring colour is a $\Pi^0_2$ property, so by $\Sigma^0_2\ind$ we can find a ${\preceq}$-minimal recurring colour $p_0$.

We now define a sequence $(u_i,v_i)_{i \in \Nn}$ by primitive recursion on $i$. Let $(u_0, v_0)$ be some pair such that $i_0 < u_0 < v_0$ and $c(u_0, v_0) = p_0$. Now assume that $u_0 < v_0 \le u_1 < v_1  \ldots \le u_i < v_i$ have been defined, $\{u_0,\ldots,u_i\}$ is homogeneous with colour $p_0$, and $\colA(u_i,v_i)= p_0$. Let $(u_{i+1}, v_{i+1})$ be the smallest pair such $v_i \le u_{i+1} < v_{i+1}$ and $\colA(u_{i+1}, v_{i+1}) = p_0$. Such a pair exists because $p_0$ is recurring. We know that $\colA(u_i,u_{i+1}) = p_0$, since on the one hand $\colA(u_i,u_{i+1}) \preceq \colA(u_i,v_i) = p_0$, and on the other hand $u_i > i_0$ and thus  $\colA(u_i,u_{i+1})$ is a recurring colour, so it cannot be $\preceq$-strictly smaller than $p_0$. Similarly, for $j<i$ we know that $\colA(u_j,u_{i+1}) = p_0$ because $\colA(u_j,u_{i+1}) \preceq p_0$ and $u_j > i_0$. Therefore, the set $\{u_i\mid i \in \Nn\}$ is homogeneous for $\colA$.

Before proceeding to prove the additive version of the theorem, we recall a few basic facts about finite semigroups we shall use in our proof. The facts are proved by elementary combinatorial arguments which readily formalise in $\rca$. The proofs can be found for instance in [15].

Green preorders over a semigroup $S$ are defined as follows

* $s \le_{\GrR} t$ if and only if $s=t$ or $s \in t *S=\{t * a\mid a\in S\}$,

* $s \le_{\GrL} t$ if and only if $s=t$ or $s \in S *t=\{a * t\mid a\in S\}$,

* $s \le_{\GrH} t$ if and only if $s \le_{\GrR} t$, and $s \le_{\GrL} t$.

The associated equivalence relations are written $\GrR$, $\GrL$, $\GrH$; their equivalence classes are called respectively $\GrR$, $\GrL$, and $\GrH$-classes.

For every finite semigroup $S$ and $s, t \in S$, $s \le_{\GrL} t$ and $s \GrR t$ implies $s \GrH t$.

If $(S, {*})$ is a finite semigroup, $H\subseteq S$ an $\GrH$-class, and some $a,b\in H$ satisfy $a*b\in H$ then for some $e\in H$ we know that $(H, {*}, e)$ is a group.

Now we can prove our main statement.

Theorem <ref>
Let a colouring $\colA$ take values in the finite semigroup $(S,{*})$ and satisfy the additivity condition of Definition <ref>. For every position $i$ and every $k \geq j > i$, let us observe that $\colA(i,k) \le_{\GrR} \colA(i, j)$. Let $r$ be the function mapping every element of $S$ to its $\GrR$-class. The function $r \circ \colA$ is an ordered colouring; let us use Lemma <ref> to obtain a homogeneous sequence $(u_i)_{i \in \Nn}$ for $r \circ \colA$.

Since $S$ is finite, we can use $\Sigma^0_2$-collection to prove that there is some colour $a$ such that $\colA(u_0,u_{i}) = a$ for infinitely many $i$. This lets us take a subsequence $(v_i)_{i \ge 0}$ of $(u_i)_{i \ge 0}$ such that $\colA(v_0,v_{i})=a$ for each $i$.

We now know that $a = a * \colA(v_i, v_j)$ for every $0 < i < j$. In particular, $a \le_{\GrL} \colA(v_i, v_j)$ by the definition of ${\le_{\GrL}}$. Since $a$ and $\colA(v_i, v_j)$ are $\GrR$-equivalent, Lemma <ref> implies that $\colA(v_i, v_j) \GrH a$. Let $H$ be the $\GrH$-class of $a$. Since $a*\colA(v_i,v_j)=a\in H$ we know by Lemma <ref> that $(H,{*},e)$ is a group for some $e\in H$. Using this group structure and the equation $a = a * \colA(v_i, v_j)$ we obtain that $\colA(v_i, v_j)=e$. Hence, $\{v_{i+1} \mid i \in \Nn \}$ is a homogeneous set for $\colA$ with the colour $e$.

We will now sketch the opposite implication, as stated by the following lemma. It follows from the other implications of Theorem <ref>, thus the reasoning presented here is not needed to obtain the theorem. However, we decided to include it, as the argument is very straightforward and avoids the use of automata and logic.

Over $\rca$, Additive Ramsey's Theorem implies $\Sigma^0_2\ind$.

By the construction from Section <ref>, a failure of $\Sigma^0_2\ind$ gives us $a\in\Nn$ and an infinite word $\infA\in\{0,\ldots,a+1\}^\Nn$ such that there is no highest letter $i$ that appears infinitely many times in $\infA$. Fix such a word $\infA$ and consider the colouring with values in $\{0,\ldots,a+1\}$ defined for $i<j$ as follows:

\[\colA(i,j)=\max\{\infA(k)\mid i\leq k<j\}.\]

Clearly, $\colA$ is an additive colouring of $[\Nn]^2$ by elements of the semigroup $(\{0,\ldots,a+1\}, {\max})$. Apply Additive Ramsey's Theorem to obtain an infinite homogeneous set $I\subseteq\Nn$ for $\colA$. Assume that $i\in\{0,\ldots,a+1\}$ is the colour of $I$. By the definition of $\colA$, $i$ is the highest colour that appears infinitely many times in $\infA$.

Additionally, in Appendix <ref> we provide a direct proof that Ordered Ramsey's Theorem implies $\Sigma^0_2\ind$.

§ ADDITIVE RAMSEY IMPLIES COMPLEMENTATION

In this section, we sketch a proof of the following theorem.

The proof of this theorem follows the standard construction of the automaton $\Bb$ [3]: the states of $\Bb$ are based on transition matrices of $\Aa$ (see Section <ref>). The automaton $\Bb$ guesses a Ramseyan decomposition of the given infinite word $\infA$ with respect to a certain homomorphism into $[Q]$; and then verifies that the decomposition witnesses that there cannot be any accepting run of $\Aa$ over $\infA$. A complete proof of the theorem is given in Appendix <ref>.

§ COMPLEMENTATION IMPLIES DECIDABILITY

The proof of this theorem is given in Appendix <ref>. Te argument is along the lines of the standard inductive construction of an automaton $\Aa_\phi$ that simulates the behaviour of $\phi$. Let us recall that in $\rca$ we only have truth definitions for fixed-depth formulae. Additionally, each such truth definition is not a $\Sigma^0_1$ formula (it is not even arithmetical, as it quantifies over infinite words). Therefore, in $\rca$ we cannot perform any induction involving the truth definition. This fact has two consequences:

* in the above theorem, the implication from complementation to decidability is stated for all $n\in \omega$ separately and its proof is obtained via an external induction over $n$,

* our construction of $\Aa_\phi$ needs to work in a fixed number of steps (depending on $n$), no iterative procedure can be involved. In particular, we need to simulate whole blocks of quantifiers or connectives at once.

To complete the proof of the theorem, we verify in $\rca$ that the emptiness problem is decidable for Büchi automata, as expressed by the following lemma.

§ DECIDABILITY IMPLIES IND

In this section we prove the following theorem.

The rest of this section is devoted to a proof of this theorem. Consider a $\Pi^0_2$ formula (with parameters we keep implicit)
$\phi(i) \equiv \forall x \, \exists y. \ \delta(i,x,y)$ and suppose it satisfies the premises of induction, i.e. $\phi(0)$ holds and $\forall i \, (\phi(i) \Rightarrow \phi(i + 1))$. Take $a\in\Nn$. We want to show that $\phi(a)$ holds. For that we will use decidability of the depth-$5$ fragment of $\mso(\Nn,{\le})$ to prove using $\Sigma^0_1\ind$ that a certain formula $\psi_{a+1}$ is true in $(\Nn, {\le})$. We will construct a specific infinite word that encodes the semantics of $\phi(a)$ and use the fact that the word  satisfies $\psi_{a+1}$ to deduce that $\phi(a)$ holds.

For $k\in\Nn$ let $\psi_k$ be the $\mso$ formula stating “for every infinite word over the alphabet $\{0,\ldots,k\}$ there is a maximal letter $i\in\{0,\ldots,k\}$ occurring infinitely often”. More formally, $\psi_k$ is defined as follows.

\begin{align}
\psi_k \equiv&\quad \forall X_0\, \forall X_1\, \ldots \forall X_k\, \left[\forall x\, \left( \bigvee_{i\le k} x\in X_i \land \bigwedge_{i<j\le k} \lnot\big(x\in X_i\land x\in X_j\big)\right)\right.\Longrightarrow\label{eq:formula}\\
&\left.\quad \bigvee_{i \le k} \left((\forall x \, \exists y\! \ge\! x.\ y\in X_i) \wedge \bigwedge_{i<j\le k} (\exists x \, \forall y\!\ge\! x. \ y\notin X_j)\right)\right].\nonumber
\end{align}

The formula $\psi_k$ is an formula of depth $5$. By the assumption on decidability, the property that $\psi_k$ belongs to the theory $\mso(\Nn, {\le})$ can be expressed by a $\Sigma^0_1$ formula of second-order arithmetic, $\Psi(k)$ (and, in fact, by a $\Pi^0_1$ formula as well). Clearly, in $\rca$ we can prove that $\psi_0$ belongs to $\mso(\Nn,{\le})$ and for every $i\in\Nn$, if $\psi_i$ belongs to $\mso(\Nn,{\le})$, then $\psi_{i+1}$ belongs to $\mso(\Nn,{\le})$. Therefore, by the assumption on $\Psi$, we know that $\Psi(0)$ holds and $\forall i\, (\Psi(i)\Rightarrow\Psi(i+1))$. Then, $\Sigma^0_1\ind$ guarantees that $\Psi(a+1)$ is true and hence $\psi_{a+1}$ belongs to $\mso(\Nn,{\le})$.

Now our aim is to construct a specific infinite word $\infA$ over the alphabet $\{0,\ldots,a+1\}$ in such a way to guarantee that Claim <ref> below holds.

For $i\leq a$ and $w\in\Nn$ let $C(i,w)=\max\big\{v\leq w\mid \forall x\!<\!v\, \exists y\!<\! w.\ \delta(i,x,y)\big\}$.

Clearly the function $C(i,w)$ is computable. Assume a computable enumeration[$(n, k) \mapsto \frac{(n + k + 1)(n + k)}{2} + k$ is one such map simple enough.] for pairs $\fun{\lbracket \cdot , \cdot \rbracket}{\Nn^2}{\Nn}$ that is monotone with respect to the coordinatewise order on $\Nn^2$. Define an infinite word

\[\infA(n) =
\begin{cases}
i+1 & \text{if $n=\lbracket i, w \rbracket$, $i\leq a$,}\\
& \text{ and $C(i,w)>\big|\{w'<w\mid\infA(\lbracket i, w'\rbracket)=i+1\}\big|$,}\\
0 & \text{otherwise}.
\end{cases}
\]

Again, $\infA(n)$ is computable so $\alpha$ can be defined by $\Delta^0_1$-comprehension. We will prove in $\rca$ the following claim.

For every $i\le a$ and $v\in\Nn$ the letter $i+1$ appears at least $v$ times in $\infA$ if and only if $\forall x\!<\!v\, \exists y.\ \delta(i,x,y)$. In particular, $i+1$ appears infinitely many times in $\infA$ if and only if $\phi(i)$ holds.

First assume that $\forall x\!<\!v\, \exists y.\ \delta(i,x,y)$ holds for some $i\leq a$ and $v\in\Nn$. By $\Sigma^0_1$-collection, there exists some $w$ such that $\forall x\!<\!v \, \exists y\!<\!w.\ \delta(i, x, y)$. Let $k=\big|\{w'<w\mid\infA(\lbracket i, w'\rbracket)=i+1\}\big|$. If $k\geq v$ then we are done. Assume the contrary and notice that $C(i,w)\geq v$. This means that for $w'=w,w+1,\ldots,w+v-k-1$ we have $\infA(\lbracket i, w'\rbracket)=i+1$ (we use $\Sigma^0_1\ind$ to prove this). In total this gives us $v$ positions of $\infA$ that are labelled by $i+1$.

Now assume that there are at least $v$ positions of $\infA$ labelled by $i+1$. Let $w_0$ be the minimal position such that $\big|\{w'\leq w_0\mid\infA(\lbracket i, w'\rbracket)=i+1\}\big|= v$.

In particular we know that $\infA(\lbracket i, w_0\rbracket)=i+1$ and $\big|\{w'<w_0\mid\infA(\lbracket i, w'\rbracket)=i+1\}\big|= v-1$. This means that $C(i,w_0)\geq v$. By the definition of $C(i,w)$, it follows that $\forall x\!<\!v\, \exists y.\ \delta(i,x,y)$ holds.

Now we conclude the proof of Theorem <ref>. Since $\psi_{a+1}$ holds, we know that its body holds for the sets $X_i$ defined as $X_i=\{j\mid \infA(j)=i\}$, $i=0,\ldots,a+1$ ($\Delta^0_1$-comprehension is used here). Clearly these sets form a partition of $\Nn$ and thus the formula $\psi_{a+1}$ gives us an index $i\leq a+1$ such that $i$ is the maximal letter that appears infinitely many times in $\infA$. Since $\phi(0)$ holds we know that $i>0$. If $i=a+1$ then by Claim <ref> we obtain our thesis that $\phi(a)$ holds. Assume to the contrary that $i<a+1$. By Claim <ref> it means that $\phi(i)$ and $\lnot\phi(i+1)$ hold. This contradicts the assumption that $\forall i\, \big(\phi(i)\Rightarrow\phi(i+1)\big)$. Thus, a proof of $\phi(a)$ is concluded.

The work of Sections <ref>–<ref> shows that the effectivity condition in Item <ref>. of Theorem <ref> is not necessary to derive the other items in $\rca$. The bare statement that for every Büchi automaton there exists a complementing automaton already suffices.

The argument is as follows: assuming that each Büchi automaton can be complemented, the fixed-depth expressible property that a given word $\infA$ does not satisfy the body of a formula
$\psi_{k}$ as in (<ref>) can be recognised by a Büchi automaton. By the proof of Lemma <ref>, if such an automaton accepts some infinite word, then it accepts an ultimately periodic infinite word. But this clearly shows that $\psi_k$ is true for any $k$, thus proving $\Sigma^0_2\ind$ and hence also the other items of Theorem <ref>.

§ IND IMPLIES BOUNDED-WIDTH KÖNIG

$\rca + \Sigma^0_2\ind$ is too weak to prove Weak König's Lemma (in fact, $\Sigma^0_2\ind$ and $\wkl$ are incomparable over $\rca$). However, it turns out that $\Sigma^0_2\ind$ proves a restricted version of the lemma, where the “width” of the trees under consideration is globally bounded, in the sense that the subtree rooted in
a vertex $\tuple{i_0,\ldots,i_{\ell}} \in \{0,\ldots,k\}^*$ is completely determined by $i_\ell$.

Let us fix a graph $G$ with vertices contained in $Q\times \Nn$ for some finite set $Q$. The usual way of proving König's Lemma starts by defining the subset $G'$ of those vertices $v$ of $G$ for which the subgraph under $v$ is infinite. Having defined $G'$, we inductively pick any infinite path in $G'$ and—assuming $G$ does in fact contain arbitrarily long finite paths starting in $Q \times \{0\}$—we are guaranteed not to get stuck. The issue is whether we can obtain $G'$ by $\Delta^0_1$-comprehension.

A $\Pi^0_1$ definition of $G'$ is provided by a standard trick used in the context of $\wkl$. Notice that for every fixed $n$ there can be at most $|Q|$ vertices of $G$ of the form $(q,n)$. Thus a vertex $(q,n)$ is in $G'$ if and only if it has the $\Pi^0_1$ property that for every $n'\geq n$ there exists a vertex $(q',n')$ reachable from $(q,n)$ by a path in $G$.

What remains is to give a $\Sigma^0_1$-definition of $G'$.

Consider two numbers $n<m$ and a vertex $v=(q,n)$ of $G$. We will say that $v$ dies before $m$ if there is no path in $G$ from $v$ that reaches a vertex of the form $(q',m)$. For $i=0,1,\ldots,|Q|$ we will say that $i$ vertices die infinitely many times if

\begin{align*}
\forall k\, \exists n\!>\!k\, \exists m\!>\!n.\ \text{there are at least $i$ vertices of the form $(q,n)$}\\
\text{that die before $m$.}
\end{align*}

Notice that the property of $i$ that $i$ vertices die infinitely many times is $\Pi^0_2$. Clearly if $i<i'$ and $i'$ vertices die infinitely many times then $i$ vertices die infinitely many times. By $\Sigma^0_2\ind$ we can fix $i_0$ as the maximal $i$ such that $i$ vertices die infinitely many times. Notice that for each $i>i_0$ there exists $k(i)$ such that for every $m>n>k(i)$ there are fewer than $i$ vertices of the form $(q,n)$ that die before $m$. By $\Sigma^0_2$-collection, we can find a global bound $k_0$ such that $k_0>k(i)$ for all $i>i_0$. This means that for $m>n>k_0$ we have at most $i_0$ vertices of the form $(q,n)$ that die before $m$. Additionally, for infinitely many $n$ there is $m>n$ such that exactly $i_0$ vertices of the form $(q,n)$ die before $m$. The following claim shows how one can find a witness that the subgraph under a vertex $v$ is infinite.

Assume that we are given $m>n>k_0$ and a vertex $v=(q,n)$ such that exactly $i_0$ vertices of the form $(q',n)$ with $q'\neq q$ die before $m$. Then the subgraph under $v$ is infinite.

Assume to the contrary that for some $m'>m$ there is no vertex of the form $(q',m')$ that can be reached from $(q,n)$ by a path in $G$. It means that $(q,n)$ dies before $m'$. Therefore, there are at least $i_0+1$ vertices of the form $(q',n)$ that die before $m'$. This contradicts the way $k_0$ was chosen.

Clearly, if for some $m>n$ and a vertex $v=(q,n)$ we know that $v$ dies before $m$ then the subgraph of $G$ under $v$ is finite.

We shall now use Claim <ref> to give a $\Sigma^0_1$-definition of $G'$. We will say that $v=(q,n_0)$ belongs to $G'$ if there exist $m>n>\max(k_0,n_0)$ and $i_0$ vertices of the form $(q',n)$ such that all of them die before $m$ and some other vertex of the form $(q'',n)$ is reachable in $G$ by a path from $v$. Clearly this is a $\Sigma^0_1$-definition. It remains to prove that it defines $G'$. First assume that $v$ satisfies the above property and fix $m$, $n$, and $(q'',n)$ as in the definition. By Claim <ref> we know that the subgraph under $(q'',n)$ is infinite. Since $(q'',n)$ is reachable from $v$ in $G$, this implies that also the subgraph under $v$ is infinite and thus $v\in G'$. Now assume that $v=(q,n_0)\in G'$. By the choice of $i_0$ we know that there exist $m>n>\max(n_0,k_0)$ and exactly $i_0$ vertices of the form $(q',n)$ that die before $m$. Since the subgraph under $v$ is infinite, we know that some vertex of the form $(p,m)$ is reachable from $v$ in $G$. Notice that any path connecting $v$ and $(p,m)$ needs to contain a vertex of the form $(q'',n)$. Clearly $(q'',n)$ cannot be any of the $i_0$ vertices that die before $m$. Thus $v$ satisfies the above condition.

If a vertex $(q,0)$ of $G$ satisfies the hypothesis of Bounded-width König's Lemma, then $(q,0) \in G'$. Moreover, if $v=(q,n)\in G'$ then there exists $(q',n+1)\in G'$ such that there is an edge between $(q,n)$ and $(q',n+1)$.

Now, given $(q,0)\in G'$, we can construct an infinite path in $G'$ using $\Delta^0_1$-comprehension. Fix any linear order on $Q$. Let $\patA(0)$ be $(q,0)$. If $\patA(n)$ is defined let $\patA(n+1)=(q',n+1)$ for the  minimal $q' \! \in \! Q$ satisfying: $(q',n+1)\in G'$ and there is an edge in $G$ between $\patA(n)$ and $(q',n+1)$. Fact <ref> implies that $\patA$ is well-defined. By the construction $\patA$ is an infinite path in $G'$ and thus in $G$.

§ IND IMPLIES DETERMINISATION

In this section we will show the following theorem.

The proof scheme presented here is based on a determinisation procedure proposed in [14] (see [1, 9] for similar arguments and a comparison of this determinisation method to the method of Safra). Our exposition follows lecture notes of M. Bojańczyk [2].
Although the general structure of the argument is standard, we need to take additional care to ensure that the reasoning can be conducted in $\rca$ using only $\Sigma^0_2\ind$.

The proof of Theorem <ref> will be split into separate steps that will allow us to successively simplify the objects under consideration. To merge these steps we will use the notion of a deterministic transducer that transforms one infinite word into another.

A transducer is a deterministic finite automaton, without accepting states, where each transition is additionally labelled by a letter from some output alphabet. More formally, a transducer with an input alphabet $\Sigma$ and an output alphabet $\Gamma$ is a tuple $\Tt=\langle Q, q_\init, \delta\rangle$ where $q_\init\in Q$ is an initial state and $\fun{\delta}{Q\times \Sigma}{\Gamma\times Q}$.

A transducer naturally defines a function $\fun{\Tt}{\Sigma^\Nn}{\Gamma^\Nn}$. Formally, such a function is a third-order object and thus not available in second-order arithmetic. However, given a word $\alpha$, we can use $\Delta^0_1$-comprehension to obtain the unique infinite word produced by $\Tt$ on input $\infA$. Whenever we write $\Tt(\infA)$, we have this word in mind.

It is easy to see that a transducer can be used to reduce the question of acceptance from one deterministic automaton to another, as stated by the following lemma.

For every deterministic Rabin automaton $\Aa$ with the input alphabet $\Gamma$, and every transducer $\fun{\Tt}{\Sigma^\Nn}{\Gamma^\Nn}$, there exists a deterministic Rabin automaton $\Aa\circ\Tt$ which accepts an infinite word $\infA \in \Sigma^\Nn$ if and only if $\Aa$ accepts $\Tt(\infA)$.

One of the steps in the proof of Theorem <ref>, expressed by the lemma below, allows us to work with a fixed alphabet that depends only on the set of states of the given automaton $\Bb$. For that, we introduce a notion of a $Q$-dag. A $Q$-dag is an infinite word over the alphabet of transition matrices $[Q]$ of $\Bb$ that represents all the possible runs of $\Bb$ over a given infinite word, see Figure <ref> (a formal definition will be given in the full paper).

A $Q$-dag and a single letter from the alphabet $[Q]$. The accepting edges are represented by solid lines, and non-accepting edges are dashed lines.

This lemma is trivial—the transducer $\Tt_1$, after reading a finite word $w\in\Sigma^\ast$, stores in its state the set of states of $\Bb$ reachable from $q_\init^\Bb$ over $w$. The initial state of $\Tt_1$ is $\{q_\init\}$. Given a state $R\subseteq Q$ of $\Tt_1$ and a letter $a$, the transducer moves to the state

\[R'=\{q'\mid (q,a,q')\in\delta^\Bb\}\]

and outputs a letter $M\in [Q]$ such that $M(q,q')=M_a(q,q')$ if $q\in R$ and $M(q,q')=\trNon$ if $q\notin R$ (see Section <ref> for the definition of $M_a$ and $[Q]$). Clearly there is a computable bijection between the accepting runs of $\Bb$ over $\infA$ and accepting paths in the $Q$-dag $\Tt_1(\infA)$.

The next lemma shows that one can use a transducer to reduce general $Q$-dags to so-called tree-shaped $Q$-dags—the graph structure of such a word has the shape of a tree, see Figure <ref>.

A tree-shaped $Q$-dag.

To prove this lemma one uses a lexicographic order on paths in a given $Q$-dag. A crucial ingredient here is Bounded-width König's Lemma from Section <ref>. Additionally, we need to make sure that the graph to which Bounded-width König's Lemma is applied can be obtained using $\Delta^0_1$-comprehension. For this purpose we use $\Sigma^0_2\ind$ once again.

The proof of Theorem <ref> is concluded by the following lemma and an application of Lemma <ref>.

§ CONCLUSIONS AND FURTHER WORK

In this work we have characterised the logical strength of Büchi's decidability theorem and related results over the theory $\rca$. We proved over $\rca$ that complementation for Büchi automata is equivalent to $\Sigma^0_2\ind$, as is the decidability of $\mso(\Nn,{\le})$ (to the extent that this can be expressed).

Without $\Sigma^0_2\ind$, many aspects of automata on infinite words seem to make little sense (note, for instance, that the very concept of “a state occurs only finitely often” is $\Sigma^0_2$).
The picture suggested by our work is that this minimal reasonability condition already suffices to prove all the basic results. This situation is completely different for automata on infinite trees, where the concepts also make sense already in $\rca + \Sigma^0_2\ind$, but proving the complementation theorem or decidability of requires much more [10].

We are thus led to the general question whether the entire theory of automata on infinite words requires exactly $\rca + \Sigma^0_2\ind$. This includes in particular the following issues:

* Does McNaughton's determinisation theorem imply $\Sigma^0_2\ind$ over $\rca$?

* How much axiomatic strength is needed to develop the algebraic approach to (<cit.>), for instance to prove that Büchi-recognisability is equivalent to recognisability by finite Wilke algebras?

* What about developing the  Wagner hierarchy (see <cit.>)?

* Does $\rca + \Sigma^0_2\ind$ prove the uniformisation theorem for automata, in the form: for a given automaton $\Aa$ over the alphabet

$\{0,1\}^2$ such that $\forall X\,\exists Y\, (\text{$\Aa$ accepts $X\otimes Y$})$, there

exists an automaton $\Bb$ such that $\forall X\,\exists! Y\, (\text{both $\Aa$ and $\Bb$ accept $X\otimes Y$})$ (see <cit.>)?

[1]
Christoph Schulte Althoff, Wolfgang Thomas, and Nico Wallmeier.
Observations on determinization of Büchi automata.
Theor. Comput. Sci., 363(2):224–233, 2006.

[2]
Mikołaj Bojańczyk.
Lecture notes on languages, automata and computations, University of
<http://www.mimuw.edu.pl/ bojan/20152016-2/jezyki-automaty-i-obliczenia-2/mcnaughtons-theorem>.

[3]
J. Richard Büchi.
On a decision method in restricted second order arithmetic.
In Ernest Nagel, Patrick Suppes, and Alfred Tarski, editors, Logic, Methodology and Philosophy of Science. Proceeding of the 1960
International Congress, pages 1 – 11. Stanford University Press, 1962.

[4]
Thomas Colcombet and Konrad Zdanowski.
A tight lower bound for determinization of transition labeled
Büchi automata.
In ICALP (2), pages 151–162, 2009.

[5]
Petr Hájek and Pavel Pudlák.
Metamathematics of first-order arithmetic.
Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1993.

[6]
Denis R. Hirschfeldt.
Slicing the truth, volume 28 of Lecture Notes Series.
Institute for Mathematical Sciences. National University of Singapore.
World Scientific, 2015.

[7]
Jeffry L. Hirst.
Combinatorics in Subsystems of Second Order Arithmetic.
PhD thesis, Pennsylvania State University, 1987.

[8]
Carl G. Jockusch, Jr.
Ramsey's theorem and recursion theory.
J. Symbolic Logic, 37:268–280, 1972.

[9]
Detlef Kähler and Thomas Wilke.
Complementation, disambiguation, and determinization of Büchi
automata unified.
In ICALP, pages 724–735, 2008.

[10]
Leszek Aleksander Kołodziejczyk and Henryk Michalewski.
How unprovable is Rabin's decidability theorem? (accepted@LICS
CoRR, abs/1508.06780, 2015.

[11]
G. Kreisel.
A variant to Hilbert's theory of the foundations of arithmetic.
British J. Philos. Sci., 4:107–129, 1953.

[12]
Jiayi Liu.
${\mathsf{RT}}^2_2$ does not imply ${\mathsf{WKL}}_0$.
J. Symbolic Logic, 77(2):609–620, 2012.

[13]
Robert McNaughton.
Testing and generating infinite sequences by a finite automaton.
Information and Control, 9(5):521 – 530, 1966.

[14]
David E. Muller and Paul E. Schupp.
Simulating alternating tree automata by nondeterministic automata:
New results and new proofs of the theorems of Rabin, McNaughton and
Theoretical Computer Science, 141(1–2):69 – 107, 1995.

[15]
Dominique Perrin and Jean-Éric Pin.
Infinite words : automata, semigroups, logic and games.
Pure and Applied Mathematics. London, San Diego (Calif.), 2004.

[16]
Alexander Rabinovich.
On decidability of monadic logic of order over the naturals extended
by monadic predicates.
Information and Computation, 205(6):870–889, 2007.

[17]
Saharon Shelah.
The monadic theory of order.
Ann. of Math. (2), 102(3):379–419, 1975.

[18]
Stephen G. Simpson.
Subsystems of second order arithmetic.
Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1999.

§ PROOF OF THEOREM <REF> FROM SECTION <REF>

In this section we prove the following theorem.

Let us fix a Büchi automaton $\Aa=\langle Q, \Sigma, q_\init, \delta, F\rangle$. We will introduce a structure of a semigroup over the transition matrices of $\Aa$ (see Section <ref>). Let us define the natural operations of addition and multiplication over $\{\trNon,\trYes,\trAcc\}$ as depicted on Figure <ref>. The addition allows to choose preferred run (i.e. an accepting transition is better than a non-accepting one) and the multiplication corresponds to concatenation of runs.

[scale=0.5, every node/.style=scale=0.8]
(sero) at (-0.5,+0.5);

in 0,1,2,3
($(sero)+(0.5,-0.5)+(-1,-\z)$) – ($(sero)+(0.5,-0.5)+(3,-\z)$);
($(sero)+(0.5,-0.5)+(\z,+1)$) – ($(sero)+(0.5,-0.5)+(\z, -3)$);

at ($(sero) + (+0,-0)$) ${+}$;
at ($(sero) + (+1,-0)$) $\trNon$;
at ($(sero) + (+2,-0)$) $\trYes$;
at ($(sero) + (+3,-0)$) $\trAcc$;

at ($(sero) + (+0,-1)$) $\trNon$;
at ($(sero) + (+1,-1)$) $\trNon$;
at ($(sero) + (+2,-1)$) $\trYes$;
at ($(sero) + (+3,-1)$) $\trAcc$;

at ($(sero) + (+0,-2)$) $\trYes$;
at ($(sero) + (+1,-2)$) $\trYes$;
at ($(sero) + (+2,-2)$) $\trYes$;
at ($(sero) + (+3,-2)$) $\trAcc$;

at ($(sero) + (+0,-3)$) $\trAcc$;
at ($(sero) + (+1,-3)$) $\trAcc$;
at ($(sero) + (+2,-3)$) $\trAcc$;
at ($(sero) + (+3,-3)$) $\trAcc$;

(sero) at (+6.5,+0.5);

in 0,1,2,3
($(sero)+(0.5,-0.5)+(-1,-\z)$) – ($(sero)+(0.5,-0.5)+(3,-\z)$);
($(sero)+(0.5,-0.5)+(\z,+1)$) – ($(sero)+(0.5,-0.5)+(\z, -3)$);

at ($(sero) + (+0,-0)$) ${*}$;
at ($(sero) + (+1,-0)$) $\trNon$;
at ($(sero) + (+2,-0)$) $\trYes$;
at ($(sero) + (+3,-0)$) $\trAcc$;

at ($(sero) + (+0,-1)$) $\trNon$;
at ($(sero) + (+1,-1)$) $\trNon$;
at ($(sero) + (+2,-1)$) $\trNon$;
at ($(sero) + (+3,-1)$) $\trNon$;

at ($(sero) + (+0,-2)$) $\trYes$;
at ($(sero) + (+1,-2)$) $\trNon$;
at ($(sero) + (+2,-2)$) $\trYes$;
at ($(sero) + (+3,-2)$) $\trAcc$;

at ($(sero) + (+0,-3)$) $\trAcc$;
at ($(sero) + (+1,-3)$) $\trNon$;
at ($(sero) + (+2,-3)$) $\trAcc$;
at ($(sero) + (+3,-3)$) $\trAcc$;

Two operations on $\{\trNon, \trYes,\trAcc\}$ that induce multiplication on $[Q]$.

Now, given two transition matrices $M,N\in [Q]$ we can naturally define the matrix $M * N$ that is obtained by the standard matrix multiplication formula. Let $1_{[Q]}$ denote the matrix with $\trYes$ on the diagonal and $\trNon$ outside of it. Notice that the mapping $\Sigma\ni a\mapsto M_a\in[Q]$ from Section <ref> can be extended to a homomorphism $\fun{\homA}{\Sigma^\ast}{[Q]}$. Clearly, for a finite word $u\in\Sigma^\ast$ and a pair of states $q,q'\in Q$ the value $\homA(u)(q,q')\in\{\trNon,\trYes,\trAcc\}$ denotes what are the possible runs of $\Aa$ over $u$ that begin in $q$ and end in $q'$.

We will say that a pair $(N,M)\in [Q]\times[Q]$ is rejecting if there is no $q_1\in  Q$ such that:

* $N * M = N$,

* $M * M=M$,

* $N(q_\init,q_1)\in\{\trYes,\trAcc\}$,

* $M(q_1,q_1)=\trAcc$.

The structure of the automaton $\Bb$ is as follows: its set of states is $([Q])^3\cup ([Q])^2\cup [Q]\cup\{q_\init\}$. Intuitively, the automaton needs to guess that a given infinite word admits a homogeneous decomposition where the initial fragment has type $N$ and the homogeneous colour is $M$, for a rejecting pair $(N,M)$. The initial state of the automaton is $q_\init$. The accepting states are $[Q]$. The automaton has the following transitions (we write $K\trans{a}K'$ for a transition $(K,a,K')\in\delta$):

* $q_\init\trans{a} (N,M,M_a)$ for all rejecting pairs $(N,M)$,

* $(N,M,K)\trans{a} (N,M,K * M_a)$,

* $(N,M,K)\trans{a} M$, if $K * M_a=N$,

* $M\trans{a} (M,M_a)$,

* $M\trans{a} M$ if $M_a=M$,

* $(M,K)\trans{a} (M,K * M_a)$,

* $(M,K)\trans{a} M$, if $K * M_a=M$.

Over $\rca$, Additive Ramsey Theorem implies that for every infinite word $\infA$ the automaton $\Aa$ accepts $\infA$ if and only if the automaton $\Bb$ does not accept $\infA$.

The rest of this section is devoted to a proof of this lemma. First assume that both $\Aa$ and $\Bb$ accept an infinite word $\infA$. Let $\rho$ be an accepting run of $\Aa$ and let $\tau$ be an accepting run of $\Bb$. Let the state $\tau(1)$ be $(N,M,K)$. Since $\tau$ is accepting, we know that infinitely many times in $\tau$ appears a state from $[Q]$. Therefore, $\infA$ can be decomposed as $\infA=u_0u_1\ldots$ such that $\homA(u_0)= N$ and for all $i>0$ we have $\homA(u_i)=M$. Let $n_i$ be the length of $u_0u_1\ldots u_i$. Our aim is to find a state $q_1$ such that for some $j>i>0$ we have $\rho(n_i)=\rho(n_j)=q_1$ and there is some $k$ such that $n_i\leq k < n_j$ and $\rho(k)\in F$. We can find such $q_1$ by a pigeonhole principle: first define $k_0=1$ and then let $k_{i+1}$ be the smallest number such that there is an accepting state in $\rho$ between $n_{k_{i}}$ and $n_{k_{i+1}}$. The sequence of $k_i$ is defined by primitive recursion, therefore can be constructed in $\rca$. By the finite pigeonhole principle, there exist $0\leq i < j\leq |Q|+1$ such that $\rho(n_{k_i})=\rho(n_{k_j})=q_1$. Since $\rho$ has an accepting state between $n_{k_i}$ and $n_{k_j}$ we know that $M(q_1,q_1)=\trAcc$. Similarly, since $N * M=N$, we know that $N(q_\init,q_1)\in\{\trYes,\trAcc\}$. It means that the pair $(N,M)$ is not rejecting, which contradicts the definition of the transitions of $\Bb$.

Now assume that the automaton $\Bb$ rejects a given infinite word $\infA$. Consider a colouring $\colA$ such that for $i<j$ we have $\colA(i,j)=\homA\big(\infA(i)\infA(i+1)\cdots\infA(j-1)\big)$. Since $\homA$ is a homomorphism, we know that $\colA$ is additive. By Additive Ramsey Theorem we know that there exists a decomposition $\infA=u_0u_1\ldots$ such that $\homA(u_0)= N$ and for all $i>0$ we have $\homA(u_i)=M$, for some $N,M\in[Q]$. As before let $n_i$ be the length of $u_0u_1\ldots u_i$. Without loss of generality we can assume that $N * M = M$ by skipping the first element of the homogeneous set. If the pair $(N,M)$ was rejecting, the automaton $\Bb$ would accept $\infA$—we would be able to define using $\Delta^0_1$-comprehension an accepting run $\tau$ of $\Bb$ over $\infA$ such that $\tau(n_i)=M$ for all $i>1$. Therefore, there exist states $q_\init$, $q_1$ as in the definition of a rejecting pair. These two states can be used to construct an accepting run $\rho$ of $\Aa$ over $\infA$, such that for every $i>0$ we have $\rho(n_i)=q_1$, as above such a run can be defined by $\Delta^0_1$-comprehension.

§ ORDERED RAMSEY IMPLIES IND

In this section we prove that $\Sigma^0_2\ind$ follows from the Ordered Ramsey Theorem.

Over $\rca$, the Ordered Ramsey Theorem implies $\Sigma^0_2\ind$.

Consider a $\Pi^0_2$ statement $\phi(x) \equiv \forall y \, \exists z.\ \delta(x,y,z)$ such that both $\phi(0)$ and $\forall x.\ \phi(x) \Rightarrow \phi(x+1)$ hold. We want to show that $\phi(a)$ holds. Let us define the following colouring by numbers between $0$ and $a+1$.

\[\colA(i,j) := \max\big\{ x\leq a+1 \mid \forall x'\!<\!x\,\forall y \!<\! i\, \exists z \!\le\! j.\ \delta(x',y,z) \big\}\quad\text{for $i<j$.}\]

Since $\delta(x,y,z)$ is $\Delta^0_0$, this is a computable colouring and hence definable by $\Delta^0_1$-comprehension.
Notice this is an ordered colouring for the usual order over numbers (i.e. for every $i<j\leq k$, $\colA(i,j) \le \colA(i, k)$).
Thus, we can use Ordered Ramsey Theorem to get an infinite homogeneous set $I \subseteq \Nn$.

Now, let us call $m$ the color of this homogeneous set $I$. It characterizes up to which point $\phi(x)$ is inductive thanks to the following facts.

For $x\leq a+1$, if $\phi(x')$ is true for every $x' < x$,  then $m \ge x$.

For every $i \in I$ and $x'<x$ we know that $\phi(x')$ implies $\forall y\!<\!i\,\exists z.\ \delta(x',y,z)$.
By $\Sigma^0_1$-collection, we get a bound $v_{x'}$ such that $\forall y\!<\!i\, \exists z\!\le\!v_{x'}.\ \delta(x',y,z)$.
Again by $\Sigma^0_1$-collection, there exists a global bound $v$ such that $\forall x'\!<\! x\, \forall y\!<\!i\,\exists z\!\le\!v.\ \delta(x',y,z)$.
Since $I$ is infinite, there exists $j \ge v$ in $I$. We can relax the bound on the existential to prove $\forall x'\!<\!x\, \forall y\!<\!i\,\exists z\!\le\!j.\ \delta(x',y,z)$.
So by the definition of the colouring, $\colA(i,j) = m \ge x$.

For any $x' < m$, $\phi(x')$ holds.

Take $x'<m$ and any $y$. Since $I$ is infinite, there exist $j > i > y$ such that $i,j\in I$, so in particular $\forall y\!<\!i\,\exists z\!\le\!j.\ \delta(x',y,z)$. Hence there exists $z$ such that $\delta(x', y, z)$ holds.

If $m = a + 1$, we can conclude by Fact <ref> that $\phi(a)$ holds. Now let us suppose that $m \le a$ and derive a contradiction.
Since $\phi(0)$ holds, $m \ge 1$ by Fact <ref>. By Fact <ref> we know that $\phi(x')$ holds for every $x' < m$. By the inductive assumption, since $\phi(m-1)$ holds, we know that $\phi(m)$ holds. Therefore, for all $x<m+1$ we have $\phi(x)$. Fact <ref> implies in that case that $m\geq m+1$, a contradiction.

This concludes the proof of Lemma <ref>.

§ PROOF OF THEOREM <REF> FROM SECTION <REF>

A minimal fragment of $\mso$

In this section, we work with formulae of the shape $\phi$ or $\psi$ given by the following grammar:

\[
\begin{array}{lcl}
\psi &:=& \forall \bar X.\ \bigwedge_{i = 0}^k \phi_i \bnfalt A \\
\phi &:=& \exists \bar X.\ \bigvee_{i = 0}^k \psi_i \bnfalt A \\
A &:=& \Sing(X) \bnfalt \min X \le \min Y \bnfalt \neg \Sing(X) \bnfalt \neg \min X \le \min Y \\
\end{array}
\]

$\Sing(X)$ means that $n \in X$ is true for a single $n$ while $\min(X) \le \min(Y)$ means that if $n \in Y$ holds, then there exists $m \le n$ such that $m \in X$ holds.
One can elementarily show via external induction over its depth that every $\mso$ formula is equivalent to a formula of same depth given by this grammar:

* First, replace every first order variable $x$ by a second-order variable $X$. $x \le y$ will be translated to $\min(X) \le \min(Y)$ and every quantification over $x$ will become a quantification over $X$ relativised to the predicate $\Sing$.

* Push negations to the level of atomic formulae.

* Finally, make conjunctions (respectively disjunctions) commute with universal (respectively existential) quantifiers.

This reduction enables us to consider formulae containing solely second-order variables and to simplify the shape of our valuations: for a formula $\phi$ with $n$ (implicitly ordered) free variables, a valuation $\nu$ is an infinite word over the alphabet $\{0,1\}^n$.

We need to show that we can build $\Aa_\phi$ and show that it verifies if $\phi$ holds. The construction is done via external induction on the depth $n\in\omega$ of the formula $\phi$[Similarly to what happens during the complementation procedure, defining the automaton and proving soundness can be done by two separate inductions; only this second part involves stronger principles than available in $\rca$ to prove the statement for $\Aa_{\lnot\phi}$.]. Let us give the additional constructions we need and the properties we require of them for this induction to go through.

* First, let us remark that weakening can be easily be implemented. Given a projection $\fun{\pi}{\{0,1\}^n}{\{0,1\}^m}$ (with $m \le n$) and an automaton $\Aa = \langle Q , \{0,1\}^m , q_\init , \delta , F \rangle$ over $\{0,1\}^m$, define $\pi^\star \Aa := \langle Q , \{0,1\}^n , q_\init , \pi^\star \delta, F \rangle$ where $\pi^\star \delta := \{ (q, a, q') \mid \exists b \in \pi^{-1}(a). \ (q, b, q') \in \delta \}$. Then it is straightforward to prove that $\pi^\star\Aa$ accepts those infinite words whose projection is accepted by $\Aa$. As a consequence, if $\phi$ is a formula with $m$ free variables satisfied by those valuations recognised by $\Aa_\phi$, we can consider it as a formula of $n > m$ variables satisfied
by those valuations recognised by $\pi^\star\Aa_\phi$.

* Let us turn to the base cases $\Sing(X)$ and $\min(X) \le \min(Y)$. Thanks to weakening, we can restrict to the setting where the alphabet is $\{0,1\}$ and $\{0,1\}^2$ respectively and use the automata $\Aa_{\Sing}$ and $\Aa_{\min}$ from Figure <ref> to recognise the proper set of valuations.

If $\satis{w}{\Sing(X)}$, then we can show using twice $\Delta^0_1\ind$ that the runs over $\infA$ stay in the initial state until encountering a $1$ and staying in the accepting state. Conversely, for a run to stay stuck in the accepting state, twice $\Delta^0_1\ind$ ensures that it encounters a single $1$ before moving on to an infinite word with only $0$.
Similarly, by $\Delta^0_1\ind$, we prove that for every run $\rho$ over $\infA \otimes \infB$ (where $\otimes$ designates the juxtaposition operations $\{0,1\}^n \times \{0,1\}^m \to \{0,1\}^{n+m}$ extended component-wise to infinite words), $\rho(i)$ is the first state if and only if $\infA(j) = \infB(j) = 0$ for every $j < i$; hence, we get into the second state if and only if $\min X \le \min Y$.

* Given automata $\Aa_i = \langle Q_i , \{0,1\}^n , q_{\init_i} , \delta_i , F_i \rangle$ for $0 \le i \le k$, we define the union automaton as $\bigvee_{0 \le i \le k} \Aa_i := \langle \{ q_0 \} \sqcup \bigsqcup_i Q_i, \{0,1\}^n, q_0, \delta' \sqcup \bigsqcup_i \delta_i, \bigsqcup F_i  \rangle$ where $\delta' = \{(q_0, a, q) \mid \exists i\!\le\! k.\ (q_{\init_i}, a, q) \in Q_i \}$.
If $\infA$ is accepted by some $\Aa_i$ by a run $\rho$ then $\rho'$ defined as $\rho'(0)=q_0$ and as $\rho$ everywhere else is an accepting run of $\bigvee_i \Aa_i$ over $\infA$. Conversely, if $\rho \in (\{ q_0 \} \sqcup\bigsqcup_i Q_i)^\Nn$ is an accepting run of $\bigvee_i \Aa_i$ over $\infA$, $\rho(1)$ belongs to $Q_i$ for some $i$. Using $\Delta^0_1\ind$, every $\rho(n)$ belongs to $Q_i$ for $n>0$ and has all the corresponding transitions in $\delta_i$. Defining $\rho'$ by $\rho'(0) = q_{\init_i}$ and as $\rho$ everywhere else yields an accepting run of $\Aa_i$ over $\infA$.

* Finally, given $\Aa = \langle Q , \{0,1\}^{n + m} , q_\init , \delta , F \rangle$, define the projection automaton $\exists \Aa := \langle Q, \{0,1\}^n, q_\init , \delta_\exists, F \rangle$ with $\delta_\exists := \{ (q, (a_1, \dots, a_n) , q') \mid \exists b.\ (q, (a_1, \dots, a_n, b_1, \dots, b_m), q') \in \delta \}$. Then one can elementarily show that $\exists \Aa$ accepts $\infA$ if and only if there exists $\infB \in (\{0,1\}^m)^\Nn$ such that $\Aa$ accepts $\infA \otimes \infB$.
Indeed, suppose that $\infA$ is accepted by $\exists \Aa$ using an accepting run $\rho \in Q^\Nn$. By the definition, it means that for every $i$, there exists $a \in \{0,1\}^m$ such that $(\rho(i), \infA(i) \otimes a, \rho(i + 1)) \in \delta$. Define an infinite word $\infB$ by picking a minimal such $a$ for $\infB(i)$ for every $i$. Then $\infA \otimes \infB$ is accepted in $\Aa$ thanks to the run $\rho$. Conversely, it is clear that an accepting run $\rho$ over $\infA \otimes \infB$ in $\Aa$ is an accepting run of $\exists \Aa$ over $\infA$.

Now, the external induction on the depth of a given formula $\phi$ can proceed using the above constructions:

* If $\phi$ is atomic, then constructions 1, 2 and possibly complementation do the job.

* If $\phi \equiv \exists \bar X.\ \bigvee_{i=0}^k \phi_i$, construction 4 and 3 ensures the recurrence go through.

* If $\phi \equiv \forall \bar X.\ \bigwedge_{i=0}^k \phi_i$, this formula is equivalent to $\neg \exists \bar X.\ \bigvee_{i=0}^k \neg \phi_i$. We use complementation twice in addition to constructions 3 and 4 to make the induction go through.

§.§ Emptiness for Büchi automata

In order to deduce decidability of $\mso(\Nn,{\le})$ from the automata construction, one needs to decide whether a given Büchi automaton over a singleton alphabet accepts the unique infinite word. It is a consequence of the decidability of the emptiness problem for Büchi automata, as expressed by the following lemma.

Consider a Büchi automaton $\Aa =\langle Q , \Sigma , q_\init , \delta , F \rangle$. The existence of a cycle that is accessible from the initial state and contains an accepting state is a decidable property; we need to check that it is equivalent to nonemptiness.

First assume that there exist:

* a path $(q_0, a_0, \ldots, \infA_{k-1}, q_k)$ with $q_0 =q_\init$,

* a cycle $(q_k, a_k, \ldots, q_{k + k' - 1}, a_{k + k' -1}, q_{k+k'})$ with $q_{k+k'}=q_k$,

* a number $m < k'$ such that $q_{k + m} \in F$.

We can then define the a word $\infA$ and an accepting run $\rho$ of $\Aa$ over $\infA$ by $\Delta^0_1$-comprehension as follows:

\[\infA'(n) =
\begin{cases}
a_n & \text{if $n < k$},\\
a_{k + i} & \text{if $n = k + jk' + i$ for some $j$ and some $i < k'$}.
\end{cases}
\]

\[\rho(n) =
\begin{cases}
q_n & \text{if $n < k$},\\
q_{k + i} & \text{if $n = k + jk' + i$ for some $j$ and some $i < k'$ when $n \geq k$}.
\end{cases}
\]

It is straightforward to check that $\rho$ is an accepting run of $\Aa$ over $\infA$.

Conversely, if $\Aa$ accepts some infinite word $\infA$ using a run $\rho$ then there are infinitely many $n$ such that $\rho(n) \in F$. Since $F$ is finite, we can define using $\Delta^0_1$-comprehension a sequence of numbers $n_0,\ldots,n_{|F|}$ such that $\rho(n_i)\in F$ for $i=0,\ldots,|F|$. In that case, there must exist $i<j\leq |F|$ such that $\rho(n_i)=\rho(n_j)\in F$. Then $(\rho(0), \infA(0), \ldots , \rho(n_i))$ is a path from $q_\init$ to the cycle $(\rho(n_i), \infA(n_i), \ldots, \infA(n_j-1), \rho(n_j))$ which witnesses that the nonemptiness condition holds for $\Aa$.

§ DETAILED PROOFS FROM SECTION <REF>

In this section we provide the remaining parts of the proof of Theorem <ref>. The rest of this section is done in $\rca$ with $\Sigma^0_2\ind$.

§.§ Transducers

For the sake of simplicity of the presentation, the proof presented here is split into several steps which allow us to successfully simplify the structures under consideration. This simplifications will be formalised using the notion of a transducer, as follows.

A transducer is a deterministic finite automaton, without accepting states, where each transition is additionally labelled by a letter from some output alphabet. More formally, a transducer with an input alphabet $\Sigma$ and an output alphabet $\Gamma$ is a tuple $\Tt=\langle Q, q_\init, \delta\rangle$ where $q_\init\in Q$ is an initial state and $\fun{\delta}{Q\times \Sigma}{\Gamma\times Q}$. Such a transducer naturally defines a function $\fun{\Tt}{\Sigma^\Nn}{\Gamma^\Nn}$.

It is easy to see that a transducer can be used to reduce the question of acceptance from one deterministic automaton to the other, as stated by the following lemma.

For every deterministic Rabin automaton $\Aa$ with the input alphabet $\Gamma$, and every transducer $\fun{\Tt}{\Sigma^\Nn}{\Gamma^\Nn}$, there exists a deterministic Rabin automaton $\Aa\circ\Tt$ which accepts an infinite word $\infA \in \Sigma^\Nn$ if and only if $\Aa$ accepts $\Tt(\infA)$.

It is enough to take as $\Aa\circ\Tt$ an automaton with the set of states being the product of the states of $\Aa$ and the states of $\Tt$. The transition function of $\Aa\circ\Tt$ follows the transitions of $\Tt$ and transitions of $\Aa$ over the letters output by $\Tt$:

\[\delta^{\Aa\circ\Tt}\big((q^\Aa,q^\Tt),a\big)=(\delta^\Aa(q^\Aa,b), q')\quad\text{where $\delta^\Tt(q^\Tt,a)=(b,q')$}.\]

The Rabin acceptance condition of $\Aa\circ\Tt$ is taken as the acceptance of $\Aa$, skipping the second coordinate of the states. Clearly $\Aa\circ\Tt$ accepts an infinite word $\infA$ if and only if $\Aa$ accepts the infinite word $\Tt(\infA)$—the run of $\Aa\circ\Tt$ over $\infA$ equals on the first coordinate the run of $\Aa$ over $\Tt(\infA)$.

§.§ Q-dags

In the exposition below we will work with infinite words representing the set of all possible runs of a nondeterministic automaton over a fixed infinite word. Let us define a $Q$-dag to be a directed acyclic graph where the set of nodes is $Q \times \Nn$ and every edge is of the form

\[((q,n), (p,n+1)) \qquad \text{for some $p,q \in Q$ and $n \in \Nn$.}\]

Furthermore, every edge is coloured by one of the two colors: “accepting” or “non accepting”. We assume that there are no parallel edges. A path in a $Q$-dag is a finite or infinite sequence of nodes connected by edges (either accepting or non-accepting). As we will see, we can assume that every $Q$-dag is rooted—there is a chosen element $q_\init\in Q$ such that all the edges of the $Q$-dag lie on a path that starts in the vertex $(q_\init,0)$. We call a vertex $(q,n)$ reachable if there is a path from $(q_\init,0)$ to $(q,n)$ in $\infA$. We say that an infinite path in a $Q$-dag is accepting if it starts in $(q_\init,0)$ and contains infinitely many accepting edges.

A $Q$-dag and a single letter from the alphabet $[Q]$. The accepting edges are represented by solid lines, and non-accepting edges are dashed lines.

Every $Q$-dag can be naturally represented as an infinite word, where the $n$-th letter encodes the set of edges of the form $((q,n),(q',n+1))$. The alphabet used for this purpose will be the set of transition matrices $[Q]$ defined in Section <ref>. An example of a $Q$-dag and a letter in $[Q]$ are depicted on Figure <ref>.

We will be particularly interested in $Q$-dags that are tree-shaped. A $Q$-dag is tree-shaped if every node $(q,n)$ has at most one incoming edge (i.e. an edge of the form $(p,n-1)$. Notice that it makes sense to say that a letter $M\in[Q]$ is tree-shaped and a $Q$-dag is tree-shaped if and only if all of its letters are tree-shaped. Figure <ref> depicts a tree-shaped $Q$-dag.

A $Q$-dag is infinite if for every $n$ there exists a path connecting the root $(q_\init,0)$ with a vertex of the form $(q',n)$. Similarly, a $Q$-dag is infinite under $(q,n)$ if for every $n'\geq n$ there exists a path connecting the vertex $(q,n)$ with a vertex of the form $(q',n')$.

A tree-shaped $Q$-dag.

§.§ Proof of Lemma <ref>

In this subsection we will show how to reduce the question whether a $Q$-dag $\infA$ contains an accepting path to the question whether a tree-shaped $Q$-dag $\Tt(\infA)$ contains an accepting path. It is expressed by the following lemma.

In the proof we will use the following definition.

For a finite path $w$ in a $Q$-dag, define its profile to be the word over the alphabet $\{\trYes,\trAcc\}\times Q^2$ which is obtained by replacing each edge $((q,n),(q',n+1))$ in $w$ by $(x,q,q')$ where $x\in\{\trYes,\trAcc\}$ is the type of the edge ($\trAcc$ for accepting and $\trYes$ for non-accepting). Let us fix any linear order ${\preceq}$ on $\{\trYes,\trAcc\}\times Q^2$ such that $(\trAcc,q,q')\prec(\trYes,p,p')$. Let ${\preceq}$ be the lexicographic order on paths induced by the order ${\preceq}$ on their profiles. We call a path $w$ optimal if it is lexicographically minimal among all paths with the same source and target.

Lemma <ref> follows from Claims <ref> and <ref>.

There is a transducer $\fun{\Tt}{[Q]^\Nn}{[Q]^\Nn}$ such that if the input is $\infA$ then $\Tt(\infA)$ is tree-shaped with the same reachable vertices as in $\infA$, and such that every finite path from the root in $\Tt(\infA)$ is an optimal path in $\infA$.

Claim <ref>
We start with the following observation about the order ${\preceq}$. Let $w,w',u,u'$ be paths in a $Q$-dag $\infA$ such that the target of $w$ (resp. $u$) is the source of $w'$ (resp. $u'$); and $w$, $u$ are of equal length. Then $ww'\preceq uu'$ if and only if $w\prec u$ or $w=u$ and $w'\preceq u'$.

Now let us define $\Tt(\infA)$ by choosing, for every vertex reachable in $\infA$ an ingoing edge that participates in some optimal path. Putting all of these edges together will yield a tree-shaped $Q$-dag as in the statement of the claim. To produce such edges, after reading the first $n$ letters, the automaton keeps in its memory the lexicographic ordering on the optimal paths leading from the root to the nodes at depth $n$.

Notice that the above proof is purely constructive and the statement of Claim <ref> involves only finite combinatorics, therefore it can be performed in $\rca$.

Let $\Tt$ be the transducer from Claim <ref>. Over $\rca$, $\Sigma^0_2\ind$ implies that if the input $\infA$ to $\Tt$ contains an accepting path then so does the output $\Tt(\infA)$.

The rest of this subsection is devoted to a proof of Claim <ref>. Let $\infA$ be an input to $\Tt$. Assume that $\patA\in (Q\times \Nn)^\Nn$ is a path that contains infinitely many accepting edges in $\infA$. A node $v$ in the $Q$-dag $\infA$ is said to be $\patA$-merging if there exists a finite path in $\Tt(\infA)$ that leads from $v$ to a vertex on $\patA$. Our aim is to define the following set of vertices in $\infA$:

\[t=\{v\in Q\times\Nn\mid \text{$v$ is $\patA$-merging}\}.\]

The above definition is clearly a $\Sigma^0_1$ definition of $t$.

Thanks to $\Sigma^0_2\ind$, there exists a $\Pi^0_1$ predicate over vertices $v$ equivalent to “$v$ is $\patA$-merging”. As a consequence, $t$ is definable by $\Delta^0_1$-comprehension.

The proof of this subclaim is similar to the proof of Theorem <ref>.

For $i=0,1,\ldots,|Q|$ we will say that $i$ is $\patA$-merging infinitely often if

\[\forall k\, \exists n\!>\!k.\ \text{there are at least $i$ $\patA$-merging vertices of the form $(q,n)$ in $\Tt(\infA)$}.\]

The above property of $i$ is clearly a $\Pi^0_2$ property. Let $i_0$ be the maximal $i\leq|Q|$ that is $\patA$-merging infinitely often. Such $i_0$ exists by $\Sigma^0_2\ind$. Clearly if $i\leq i'$ and $i'$ is $\patA$-merging infinitely often then $i$ is also $\patA$-merging infinitely often. By the definition, if $i>i_0$ then there exists $k(i)$ such that for all $n>k(i)$ there are strictly less than $i$ $\patA$-merging vertices of the form $(q,n)$ in $\infA$. By $\Sigma^0_2$-collection, we can choose $k_0$ to be the maximal of $k(i)$ for $i_0<i\leq |Q|$. It means that if $n>k_0$ then there are at most $i_0$ $\patA$-merging vertices of the form $(q,n)$ in $\Tt(\infA)$.

We can now provide a $\Pi^0_1$ definition of $t$ (actually a $\Sigma^0_1$-definition of the vertices outside $t$). A vertex $v=(q,n)$ does not belong to $t$ if $(\star)$: there exists $n'>\max(n,k_0)$ and $i_0$ vertices of the form $v_0=(q_0,n')$, $v_1=(q_1,n')$, …, $v_{i_0}=(q_{i_0},n')$ such that:

* all the vertices $v_0,\ldots,v_{i_0}$ are $\patA$-merging in $\Tt(\infA)$,

* no path from $v$ to any of $v_i$ for $i=0,1,\ldots,i_0$ exists,

* there is no path in $\Tt(\infA)$ from $v$ to a vertex of the form $(q',m)$ that lies on $\patA$ with $m\leq n'$.

The latter two conditions are decidable, while the first one is $\Sigma^0_1$. In total, the condition $(\star)$ is $\Sigma^0_1$.

We will now prove that the negation of $(\star)$ in fact defines $t$. First assume that $v=(q,n)\notin t$. Recall that there are infinitely many $n'$ such that there are exactly $i_0$ $\patA$-merging vertices of the form $(q',n')$ in $\Tt(\infA)$. In particular, there exists $n'>\max(n,k_0)$ and $i_0$ vertices of the form $v_0=(q_0,n')$, $v_1=(q_1,n')$, …, $v_{i_0}=(q_{i_0},n')$ such that all of them are $\patA$-merging. Since $v$ is not $\patA$-merging, there cannot be a path from $v$ to any of the vertices $v_i$ for $i=1,2,\ldots,i_0$. Similarly, there cannot be a path from $v$ to $\patA$. Therefore, $v$ satisfies $(\star)$.

On the other hand, assume that $v$ has the property $(\star)$ for some $n'$ and vertices $v_0,\ldots,v_{i_0}$. Assume to the contrary that $v$ is $\patA$-merging. Let it be witnessed by a path $\patA$ from $v$ to a vertex $v''=(q'',n'')$ on $\patA$. If $n''\leq n'$ then it contradicts the last item of $(\star)$. If $n''>n'$ then let $p\in Q$ be the state such that the vertex $(p,n')$ lies on the path $w$. Clearly $(p,n')$ is $\patA$-merging so it needs to be one of the vertices $v_1,\ldots,v_{i_0}$. But in that case this vertex can be reached from $v$ by a path in $\Tt(\infA)$, a contradiction.

We now apply Bounded-width König's Lemma (see Definition <ref>) to $t$. This way we obtain an infinite path $\patA'$ that is contained in $t$. Our aim is to prove that $\patA'$ contains infinitely many accepting edges. Assume to the contrary, that for some $k\in\Nn$ there is no accepting edge of the form $((p,n),(p',n+1))$ for $n>k$ on $\patA'$. Let $(p,k)$ be a vertex that belongs to $\patA'\cap Q\times\{k\}$. Since $\patA'$ is a path in $t$, we know that $(p,k)$ is $\patA$-merging. Let $w$ be a path witnessing that, denote its final vertex on $\patA$ by $(p',k')$. Since $\patA$ is accepting, we know that there is an accepting edge of the form $((r,n-1),(r',n))$ with $k<n-1$. Let $(q,n)$ be a vertex that belongs to $\patA'\cap Q\times\{n\}$. Similarly as before, we have a path $w'$ witnessing that $(q,n)\in t$ that reaches $\patA$ in a vertex $(q',n')$. That means that in $\Tt(\infA)$ there are two paths between $(p,k)$ and $(q',n')$: the first one follows $w$ and $\patA$, the second one follows $\patA'$ and $w'$. Notice that the latter path is contained in $t$. In means that the profile of the path through $\patA'$ and $w'$ is smaller than the profile of the path through $w$ and $\patA$. By the definition of the order on the profiles, since there is an accepting edge on the respective fragment of $\patA$, the corresponding fragment of the path $\patA'$ needs to contain an accepting edge. This contradicts the assumption that there is no accepting edge of the form $((p,n),(p',n+1))$ for $n>k$ on $\patA'$.

[scale=0.6,every node/.style=scale=0.8]
(0,0) – (11,0);
(0,-4) – (11,-4);

[loosely dotted] (1,0) – (1, -4);

[loosely dotted] (7,0) – (7, -4);

[dot] (lb) at (1,-4) ;
at (1,-4.3) $(p,k)$;

[dot] (lu) at (4,-0) ;
at (4,+0.3) $(p',k')$;

(lb) .. controls ++(2,1) and ++(-2,-1) .. (lu);
at (2.9,-2) $w$;

[line width=2.5, cap=round] (6,0) – (7,0);

[dot] (rb) at (7,-4) ;
at (7,-4.3) $(q,n)$;

[dot] (ru) at (10,-0) ;
at (10,+0.3) $(q',n')$;

(rb) .. controls ++(2,1) and ++(-2,-1) .. (ru);
at (8.9,-2) $w'$;

at (-0.5,0)  $\patA$;
at (-0.5,-4) $\patA'$;

An illustration to the proof of Claim <ref>. The upper horizontal line is the path $\patA$ in $\infA$ that may not be a path in $\Tt(\infA)$. The paths $w$ and $w'$ witness that $(p,k)$ and $(q,k')$ are both $\patA$-merging. The boldfaced part of $\patA$ is the chosen accepting edge that appears on $\patA$. Among the two paths from $(p,k)$ to $(q',n')$: one through $w$ and the other through $w'$; the latter belongs to $\Tt(\infA)$. Therefore, it has to have smaller profile than the former, in particular it has to contain an accepting edge in between the vertices $(p,k)$ and $(q,n)$.

This concludes the proof of Lemma <ref>.

§.§ Proof of Lemma <ref>

In this section we prove the remaining lemma that concludes the proof of Theorem <ref>.

We will start by defining the states and transitions of the constructed Rabin automaton. Then we will prove that it in fact verifies if a given infinite word that is a tree-shaped $Q$-dag contains an accepting path.

In general, the size of the constructed Rabin automaton is one of the crucial parameters of the construction, as it influences the running time of the algorithms for verification and synthesis of reactive systems. However, in this work we are mainly focused on the fact that an equivalent deterministic automaton exists. Therefore, the construction presented here will be far from optimal. For a discussion on optimality of the constructions involved, see [4].

Fix a finite nonempty set $Q$. We will say that $\tau$ is a $Q$-scheme if $\tau$ is a finite tree with:

* internal nodes labelled by $Q$,

* leaves uniquely labelled by $Q$,

* edges uniquely labelled by $\{0,1,\ldots,2\cdot|Q|\}$, these labels are called identifiers,

* each edge additionally marked as either “accepting” or “non-accepting”.

Additionally, the root cannot be a leaf and every node of $\tau$ that is not a leaf nor a root has to have at least two children. Except that, a $Q$-scheme doesn't need to be balanced as a tree.

It is easy to see that since the leaves of $\tau$ are uniquely labelled by $Q$, $\tau$ has at most $2\cdot|Q|$ nodes in total. Therefore, the requirement that the labelling by $\{0,\ldots,2\cdot|Q|\}$ needs to be pairwise distinct is not restricting. Clearly the number of $Q$-schemes is finite (in fact exponential in $|Q|$). Let the set of states of $\Aa$ be the set of all $Q$-schemes. Let the initial state of $\Aa$ be the $Q$-scheme consisting of two nodes: the root and its only child, both labelled by $q_\init$. Let the edge between the root and the unique leaf be labelled by the identifier $0$ and be “non-accepting”.

We will now proceed to the definition of transitions of $\Aa$. Assume that the automaton is in a state $\tau$ and reads a tree-shaped letter $M\in[Q]$, see Figure <ref>.

[acc] (0*, -0) edge node[above, idf] $2$ ++(, +1.5);
[tra] (0*, -0) edge node[below, idf] $3$ ++(, -1.0);

[tra] (1*, +1.5) edge node[above, idf] $9$ ++(, +0.5);
[acc] (1*, +1.5) edge node[below, idf] $6$ ++(, -0.5);
[tra] (1*, -1.0) edge node[above, idf] $5$ ++(, +1.0);
[tra] (1*, -1.0) edge node[below, idf] $7$ ++(, +0.0);
[acc] (1*, -1.0) edge node[below, idf] $1$ ++(, -1.0);

[dot] at (0*, 0) ;
[dot] at (1*, +1.5) ;
[dot] at (1*, -1.0) ;

in -2,...,2
[dot] at (2*, ) ;

in 0,...,1
in -3,...,3
[dot] at (3*+*, ) ;

[tra] (3*, +3.0) – ++(, -0.0);
[acc] (3*, +3.0) – ++(, -1.0);

[tra] (3*, +1.0) – ++(, -0.0);
[acc] (3*, +1.0) – ++(, -1.0);

[acc] (3*, -1.0) – ++(, -0.0);
[acc] (3*, -2.0) – ++(, -0.0);
[tra] (3*, -2.0) – ++(, -1.0);

A $Q$-scheme $\tau$ (a state of $\Aa$) and a successive tree-shaped letter $M\in[Q]$. The “non-accepting” edges in $\tau$ are dashed. The leafs of $\tau$ are arranged according to some fixed order on $Q$ in such a way to match the layout of $M\in[Q]$. To simplify the picture we do not write down the states in $Q$ labeling the nodes of $\tau$, instead we put dots.

(sero) at (0,0);

[acc] ($(sero)+(0*\dxs, -0)$) edge node[above, idf] $2$ ++(, +1.5);
[tra] ($(sero)+(0*\dxs, -0)$) edge node[below, idf] $3$ ++(, -1.0);

[tra] ($(sero)+(1*\dxs, +1.5)$) edge node[above, idf] $9$ ++(, +0.5);
[acc] ($(sero)+(1*\dxs, +1.5)$) edge node[below, idf] $6$ ++(, -0.5);
[tra] ($(sero)+(1*\dxs, -1.0)$) edge node[above, idf] $5$ ++(, +1.0);
[tra] ($(sero)+(1*\dxs, -1.0)$) edge node[below, idf] $7$ ++(, +0.0);
[acc] ($(sero)+(1*\dxs, -1.0)$) edge node[below, idf] $1$ ++(, -1.0);

[dot] at ($(sero)+(0*\dxs, 0)$) ;
[dot] at ($(sero)+(1*\dxs, +1.5)$) ;
[dot] at ($(sero)+(1*\dxs, -1.0)$) ;

[dot] at ($(sero)+(2*\dxs, 2)$) ;
[dot] at ($(sero)+(2*\dxs, 1)$) ;
[dot] at ($(sero)+(2*\dxs, 0)$) ;
[dot] at ($(sero)+(2*\dxs, -1)$) ;
[dot] at ($(sero)+(2*\dxs, -2)$) ;

in -3,...,1
[dot] at ($(sero)+(3*\dxs, \y)$) ;

[tra] ($(sero)+(2*\dxs, +1.0)$) – ++(, -0.0);
[acc] ($(sero)+(2*\dxs, +1.0)$) – ++(, -1.0);

[acc] ($(sero)+(2*\dxs, -1.0)$) – ++(, -0.0);
[acc] ($(sero)+(2*\dxs, -2.0)$) – ++(, -0.0);
[tra] ($(sero)+(2*\dxs, -2.0)$) – ++(, -1.0);

(sero) at (7,0);

[acc] ($(sero)+(0*\dxs, -0)$) edge node[above, idf] $2$ ++(, +1.5);
[tra] ($(sero)+(0*\dxs, -0)$) edge node[below, idf] $3$ ++(, -1.0);

[acc] ($(sero)+(1*\dxs, +1.5)$) edge node[below, idf] $6$ ++(, -0.5);
[tra] ($(sero)+(1*\dxs, -1.0)$) edge node[above, idf] $7$ ++(, +0.0);
[acc] ($(sero)+(1*\dxs, -1.0)$) edge node[below, idf] $1$ ++(, -1.0);

[dot] at ($(sero)+(0*\dxs, 0)$) ;
[dot] at ($(sero)+(1*\dxs, +1.5)$) ;
[dot] at ($(sero)+(1*\dxs, -1.0)$) ;

[dot] at ($(sero)+(2*\dxs, 1)$) ;
[dot] at ($(sero)+(2*\dxs, -1)$) ;
[dot] at ($(sero)+(2*\dxs, -2)$) ;

in -3,...,1
[dot] at ($(sero)+(3*\dxs, \y)$) ;

[tra] ($(sero)+(2*\dxs, +1.0)$) – ++(, -0.0);
[acc] ($(sero)+(2*\dxs, +1.0)$) – ++(, -1.0);

[acc] ($(sero)+(2*\dxs, -1.0)$) – ++(, -0.0);
[acc] ($(sero)+(2*\dxs, -2.0)$) – ++(, -0.0);
[tra] ($(sero)+(2*\dxs, -2.0)$) – ++(, -1.0);

(sero) at (14,0);

[acc] ($(sero)+(0*\dxs, -0)$) edge node[above, idf] $2$ ++(2*, +1.0);
[tra] ($(sero)+(0*\dxs, -0)$) edge node[below, idf] $3$ ++(, -1.0);

[acc] ($(sero)+(1*\dxs, -1.0)$) edge node[above, idf] $7$ ++(2*, +0.0);
[acc] ($(sero)+(1*\dxs, -1.0)$) edge node[below, idf] $1$ ++(, -1.0);

[dot] at ($(sero)+(0*\dxs, 0)$) ;
[dot] at ($(sero)+(1*\dxs, -1.0)$) ;

[dot] at ($(sero)+(2*\dxs, 1)$) ;
[dot] at ($(sero)+(2*\dxs, -2)$) ;

in -3,...,1
[dot] at ($(sero)+(3*\dxs, \y)$) ;

[tra] ($(sero)+(2*\dxs, +1.0)$) – ++(, -0.0);
[acc] ($(sero)+(2*\dxs, +1.0)$) – ++(, -1.0);

[acc] ($(sero)+(2*\dxs, -2.0)$) – ++(, -0.0);
[tra] ($(sero)+(2*\dxs, -2.0)$) – ++(, -1.0);

(sero) at (21,0);

[acc] ($(sero)+(0*\dxs, -0)$) edge node[above, idf] $2$ ++(2*, +1.0);
[tra] ($(sero)+(0*\dxs, -0)$) edge node[below, idf] $3$ ++(, -1.0);

[acc] ($(sero)+(1*\dxs, -1.0)$) edge node[above, idf] $7$ ++(2*, +0.0);
[acc] ($(sero)+(1*\dxs, -1.0)$) edge node[below, idf] $1$ ++(, -1.0);

[dot] at ($(sero)+(0*\dxs, 0)$) ;
[dot] at ($(sero)+(1*\dxs, -1.0)$) ;

[dot] at ($(sero)+(2*\dxs, 1)$) ;
[dot] at ($(sero)+(2*\dxs, -2)$) ;

in -3,...,1
[dot] at ($(sero)+(3*\dxs, \y)$) ;

[tra] ($(sero)+(2*\dxs, +1.0)$) edge node[above, idf] $4$ ++(, -0.0);
[acc] ($(sero)+(2*\dxs, +1.0)$) edge node[below, idf] $5$ ++(, -1.0);

[acc] ($(sero)+(2*\dxs, -2.0)$) edge node[above, idf] $6$ ++(, -0.0);
[tra] ($(sero)+(2*\dxs, -2.0)$) edge node[below, idf] $8$ ++(, -1.0);

The successive transformation of the scheme $\tau$ when performing steps $1$ to $4$ of a transition of $\Aa$.

The resulting state $\tau'$ is constructed by preforming the following four steps, the successive evolution of $\tau'$ is depicted on Figure <ref>

Step 1. We append the new letter $M$ to the $Q$-scheme $\tau$ obtaining a new tree. The identifiers on the newly created edges are undefined and some nodes may have exactly one child. However, all the nodes are labelled by the states in $Q$, either coming from $\tau$ or from $M$.

Step 2. We eliminate paths that die out before reaching the target states of $M$. In the running example, this means eliminating edges with identifiers $9$ and $5$.

Step 3. We eliminate unary nodes, thus joining several edges into a single edge. This means that a path which only passes through nodes of degree one gets collapsed into a single edge, the identifier for such an edge is inherited from the first (i.e. leftmost) edge on the path. The newly created edge is “accepting” if and only if any of the collapsed edges was “accepting”. In the running example, this means eliminating the unary nodes that are the targets of edges with identifiers $2$ and $7$.

Step 4. Finally, if there are edges that do not have identifiers, these edges get assigned arbitrary identifiers that are not currently used. In the running example we add identifiers $4$, $5$, $6$, and $8$.

This completes the definition of the state update function. We now define the acceptance condition.

*The acceptance condition. When executing a transition, the automaton described above goes from one $Q$-scheme to another $Q$-scheme. For each identifier, a transition can have three possible effects, described below:

Delete An edge can be deleted in Step 2 (it dies out) or in Step 3 (it is merged with a path to the left). The identifier of such an edge is said to be deleted in the transition. The deleted identifiers in the running example are $9$, $5$, and $6$. Since we reuse identifiers, an identifier can still be present after a transition that deletes it, because it has been added again in Step 4, e.g. this happens to identifiers $5$ and $6$ in the running example.

Refresh In Step 3, a whole path with edges identified by $e_1,e_2, \cdots, e_n$ is folded into its first edge identified by $e_1$. If any of the edges identified by $e_2, \cdots, e_n$ was “accepting” then we say that the identifier $e_1$ is refreshed. In the running example the refreshed identifiers are $2$ and $7$ (the edge identified by $2$ was already “accepting” while the edge identified by $7$ become “accepting” because of the merging.

Nothing An identifier might be neither deleted nor refreshed, e.g. this is the case for the identifier $1$ in the running example.

The following lemma describes the key property of the above data structure.

For every tree-shaped $Q$-dag $\infA\in[Q]^\omega$, the following are equivalent:

* $\infA$ contains an accepting path,

* some identifier is deleted finitely often but refreshed infinitely often.

Before proving the above lemma, we show how it completes the proof of Lemma <ref>. Clearly the second condition above can be expressed as a Rabin condition on transitions of $\Aa$—the Rabin pairs $(E_i,F_i)$ range over the set of identifiers $i=1,\ldots,2\cdot|Q|$, a transition is in $F_i$ if an edge with identifier $i$ is deleted and is in $E_i$ if the edge is refreshed.

Lemma <ref>
First assume that $\infA$ contains an accepting path $\patA$. Let $\rho$ be the sequence of states of $\Aa$ when reading $\infA$. Notice that, for every $n$ the path $\patA$ indicates a path in the $Q$-scheme $\rho(n)$ that connects the root with a leaf (labelled by a state $q(n)$ such that $\patA(n)=(q(n),n)$). Let $e^{(n)}_0,\ldots,e^{(n)}_k(n)$ be the identifiers of the edges on this path. Notice that $k(n)\leq |Q|$ because each internal node of a $Q$-scheme has at least two children and leafs of $Q$-schemes are uniquely labelled by the states in $Q$. We will say that a position $k=0,1,\ldots,|Q|$ is unstable if for infinitely many $n$ we have either $k(n)<k$ or some identifier $e^{(n)}_{k'}$ for $k'\leq k$ is deleted in the $n$-th transition in $\rho$. Notice that $0$ is stable because we never delete the first edge of a $Q$-scheme. Let $k_0$ be the greatest stable number, such a number exists by $\Sigma^0_2\ind$.

By $\Sigma^0_2$-collection we can find a number $n_0$ such that for $n\geq n_0$ we have $k(n)\geq k_0$ and no identifier $e^{(n)}_{k'}$ with $k'\leq k_0$ is deleted in the $n$-th transition in $\rho$. Therefore, for every $k'\leq k_0$ and $n\geq n_0$ we have

\[e^{(n)}_{k'}=e^{(n_0)}_{k'}.\]

Let $i=e^{(n)}_{k_0}$. Clearly by the definition of $k_0$ we know that the identifier $i$ is not deleted for $n\geq n_0$. It remains to prove that $i$ is refreshed infinitely many times. Assume to the contrary that for some $n_1\geq n_0$ and every $n\geq n_1$ the identifier $i$ is never refreshed in the $n$-th transition in $\rho$. First notice that $\patA$ contains an accepting edge of the form $((q,n_2-1),(q',n2))$ for some $n_2\geq n_1$. It means that the edge identified by $e^{(n_2)}_{k(n_2)}$ is accepting in $\rho(n_2)$—this is the last edge on the path corresponding to $\patA$ in the $Q$-scheme obtained after reading the $n_2$-th letter of $\infA$. By the definition of $k_0$ we know that for some $n_3\geq n_2$ the identifier $e^{(n_3)}_{k_0+1}$ is deleted in the $n_3$-th transition in $\rho$. Notice that since $\patA$ is an infinite path, this identifier cannot be deleted in Step 2 as it never dies out. Therefore, $k(n_3+1)=k_0$. Let us prove by $\Sigma^0_1\ind$ on $n=n_2,n_2+1,\ldots,n_3$ that either:

* the identifier $i$ is refreshed in a $n'$-th transition of $\rho$ for some $n'$ such that $n_2\leq n'\leq n$,

* there exists an accepting edge in the $Q$-scheme $\rho(n)$ that is identified by $e^{(n)}_{k'}$ for some $k'$ such that $k_0<k'\leq k(n)$.

For $n=n_2$ the second possibility holds. The inductive step follows directly from the definition of the transitions of $\Aa$—an accepting edge propagates to the left, firing successive refreshes for the merged identifiers. For $n=n_3$ we know that there is no $k'$ such that $k_0<k'\leq k(n)$ thus the first possibility needs to hold. This contradicts our assumption that there was no refresh on $i$ after the $n_2$-th letter of $\infA$ was read. This concluded the first implication in the proof of Lemma <ref>.

Now assume that $\infA$ is an infinite word such that the automaton $\Aa$ accepts it. Let us fix the run $\rho$ of $\Aa$ over $\infA$ and assume that $i_0$ is an identifier that is deleted only finitely many times but refreshed infinitely many times. Our aim is to prove that the $Q$-dag $\infA$ contains an accepting path. Again, by $\Sigma^0_2$-collection we find $n_0$ such that the identifier $i_0$ is never deleted after the $n_0$-th transition of $\Aa$.

We start by noticing that for every $n\geq 0$ and an edge identified by $e$ in the $Q$-scheme $\rho(n)$, this edge corresponds to a finite path $w_{n,e}$ in the $Q$-dag $\infA$. For the newly created edges that are assigned new identifiers in Step 4, the corresponding path is an edge $(q,n),(q',n')$ from the letter $M$. For edges that were assigned an identifier earlier, the path is defined inductively, by merging the paths whenever we merge edges in Step 3. Using $\Sigma^0_1\ind$ we easily prove that a corresponding edge is marked “accepting” if and only if the path contains an accepting edge in $\infA$. If an identifier $i$ is refreshed then the path gets longer and contains at least one new accepting transition.

In this way, we can track the path corresponding to the edges identified by $i_0$ for $n\geq n_0$. Since the identifier $i_0$ is refreshed infinitely many times, the path corresponding to it is prolonged infinitely many times. Notice that the source of the paths corresponding to $i_0$ are fixed and of the form $(q(n_0),n_0)$—the identifier $i_0$ is never merged to the left. Clearly, for every $n\geq n_0$ we can effectively assign a state $q(n)$ such that for some $n'>n_0$ the path $w_{n',i_0}$ passes through $(q(n),n)$—such $n'$ exists because $i$ is refreshed infinitely many times. It gives us a $\Delta^0_1$-definition of an infinite path $\patA$ that starts in $(q(n_0),n_0)$. Notice that each refresh of $i_0$ corresponds to a new accepting edge on $\patA$, what means that $\patA$ is accepting.