# 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. –  Carl Mummert Mar 9 '11 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. –  Alex Simpson Mar 9 '11 at 7:23

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.) –  Alex Simpson Sep 5 '13 at 10:40