The hierarchy inside closed monadic Σ1 collapses on the infinite binary tree

Closed monadic Σ₁, as proposed in (Ajtai et al., 1998), is the existential monadic second order logic where alternation between existential monadic second order quantifiers and first order quantifiers is allowed. Despite some effort very little is known about the expressive power of this logic on finite structures. We construct a tree automaton which exactly characterizes closed monadic Σ₁ on the Rabin tree and give a full analysis of the expressive power of closed monadic Σ₁ in this context. In particular we prove that the hierarchy inside closed monadic Σ₁, defined by the number of alternations between blocks of first order quantifiers and blocks of existential monadic second order quantifiers collapses, on the infinite tree, to the level 2