On the Rlationship Between Monadic and Weak Monadic Second Order Logic on Arbitrary Trees,with Applications to the mu-Calculus

Abstract

In 1970 [26], in Weakly definable relations and special automata, Math. Log. and Found. of Set Theory, pp 1-23, Rabin shows that a language is recognizable by a tree automaton with Büchi like infinitary condition if and only if it is definable as the projection of a weakly definable language. In this paper, we refine this result characterizing such languages as those definable in the monadic Σ₂ level of the quantifier alternation depth hierarchy of monadic second order logic (MSO). This new result also contributes to a better understanding of the relationship between the quantifier alternation depth of hierarchy of MSO and the fixpoint alternation depth hierarchy of the mu-calculus: it shows that the bisimulation invariant fragment of the monadic Σ₂ level equals the νμ-level of the mu-calculus hierarchy.