# Complementation of $\omega$-regular languages in reverse mathematics

Does anyone know where Büchi's theorem that $\omega$-regular languages are closed under complementation fits into the reverse-mathematics classification scheme? That is, is it equivalent over $\mathrm{RCA}_0$ to one of the usual subsystems of second-order arithmetic? Or, if not known to be equivalent, what is known about where it fits in?

The formulation I have in mind is, for a fixed finite signature $\Sigma$, the statement: for every finite automaton $M$ (over $\Sigma$), there exists a finite automaton $M^c$, such that, for every $\omega$-word $\alpha$ over $\Sigma$, it holds that $\alpha$ is (Büchi-)accepted by $M$ if and only if $\alpha$ is not accepted by $M^c$.

• I don't know the area very well. Is it the case that given a Büchi automaton one can explicitly construct a Muller automaton accepting the same language, and vice versa? If so, the theorem is most likely provable in RCAo; but I don't know the proofs so I can't check that in detail. Separately, it seems that the statement you are interested in is of a certain syntactic form (it's better than just $\Pi^1_1$) so that it will be somewhat trivially satisfied by the $\omega$-model REC (using the fact that the principle is true). So the principle cannot imply WKLo or ACAo over RCAo. Mar 9, 2011 at 4:25
• Yes from every nondeterministic Büchi automaton one can construct a deterministic Muller automaton accepting the same language (and vice versa) - this is McNaughton's Theorem. Does anyone happen to know if this proof goes through in RCAo? I also don't know the area very well (hence the question). As you say, the theorem cannot imply the stronger comprehension principles. Still, it is plausible to me that McNaughton's Theorem uses a combinatorial principle in its proof that does not hold in RCAo. I could go through the proof myself, but I'm hoping that someone already knows. Mar 9, 2011 at 7:23

This paper might be relevant: http://arxiv.org/abs/1508.06780. It studies the complementation result for automata over infinite trees, rather than words.

There is a remark in this paper (page 11) concerning determinization of Buchi automata over ω-words:

We have not attempted a careful verification, but we believe that the proof of determinization for word automata goes through in the fragment of ACA0 known as WKL0 extended by the induction scheme for Σ02 formulas. Without Σ02 induction, the basic notions of automata theory on infinite structures make little sense, in particular the lim inf of ranks appearing in a computation might not exist.

Perhaps this remark can also be of help when considering complementation.

There is a new paper addressing exactly this question:

L. A. Kołodziejczyk, H. Michalewski, P. Pradic, M. Skrzypczak, The logical strength of Büchi's decidability theorem

accepted to CSL 2016. The paper is available at the first author's website: http://www.mimuw.edu.pl/~lak/buchi_strength.pdf.

The abstract states:

We prove that the following are equivalent over the weak second-order arithmetic theory $\text{RCA}_0$:

1. Büchi’s complementation theorem for nondeterministic automata on infinite words,
2. the decidability of the depth-n fragment of the MSO theory of (N, ≤), for each n ≥ 5,
3. the induction scheme for $\Sigma^0_2$ formulae of arithmetic.
• Presumably $\Sigma^2_0$ in item 3 should be $\Sigma^0_2$. Aug 25, 2016 at 14:55

I am not familiar with all proofs of McNaughton's theorem, but the ones I have seen use the weak form of Konig's Lemma that a finitely branching infinite tree contains an infinite path.

• Yes. Similarly, Büchi's original (direct) proof of his complementation theorem used the infinite Ramsey theorem for pairs. I am still hoping, however, for a more definitive answer; e.g., an answer to the question: is Büchi's theorem provable in $\text{RCA}_0$? (Sorry for the long delay before responding to your answer.) Sep 5, 2013 at 10:40