Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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$.

share|improve this question
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

1 Answer 1

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.

share|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.