MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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|cite|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

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|cite|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

This paper might be relevant: 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.

share|cite|improve this answer

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.