# Are MSO formulae on graphs expressible with bounded quantifier alternation?

Is there some $$k$$ such that, given any formula $$\varphi$$ in the monadic second order theory of graphs (this question applies for either MSO with sets of vertices and edges or just MSO with sets of edges), there is an equivalent formula $$\psi$$ with quantifier-alternation $$k$$?

(Here I think it makes sense to count both alternation in first-order and second-order quantifiers)

This question is inspired by Are MSO formulae expressible as existential SO formulae over arbitrary structures?. Finite state automata act as a kind of canonical form for formulas in WS1S (the weak monadic second order theory of one successor). So one wonders if there's possibly some other kind of canonical form for one of the monadic second order theories of graphs.

No, for the same reason as in the linked question: an SO sentence over a given class of structures can be translated to an MSO sentence over structures augmented with their Cartesian powers, which can in turn be translated to an MSO sentence over graphs due to the universality of graphs. Thus, if MSO on graphs collapses to $$\Sigma^1_k$$, then the polynomial hierarchy collapses to $$\mathrm{PH}=\Sigma^\mathrm P_k$$.
More precisely, let $$\Phi$$ be an SO sentence in a finite signature $$L$$, quantifying over $$l$$-ary relations. Assume for simplicity that $$L$$ is relational. Let $$L'=L\cup\{P(x_1,\dots,x_l,y)\}$$, and for any $$L$$-structure $$\mathcal A=(A,\dots)$$, let $$f(\mathcal A)$$ be the $$L'$$-structure with domain $$A\mathbin{\dot\cup}A^l$$ that carries the original $$L$$-structure on $$A$$, and where $$P$$ is interpreted as the graph of the partial function that maps an $$l$$-tuple of elements of $$A$$ to the corresponding element of $$A^l$$. Notice that $$f$$ is polynomial-time computable. Then there is an MSO sentence $$\Phi'$$ such that $$\mathcal A\models\Phi\iff f(\mathcal A)\models\Phi'$$ for every $$L$$-structure $$\mathcal A$$.
Moreover, there is a polynomial-time function $$g$$ mapping $$L'$$-structures to graphs, and a $$1$$-dimensional FO interpretation $$I$$ such that for any $$L'$$-structure $$\mathcal A'$$, $$I$$ interprets $$\mathcal A'$$ in $$g(\mathcal A')$$. (There are many ways how to do that; see e.g. Hedrlín & Pultr and Miller for variants of this construction in various contexts.) Then $$\Phi'^I$$ is an MSO sentence on graphs (more precisely, $$\mathrm{MSO}_1$$, i.e., quantifying over sets of vertices) such that $$\mathcal A\models\Phi\iff g(f(\mathcal A))\models\Phi'^I.$$ If $$\Phi'^I$$ is equivalent to an $$\Sigma^1_k$$ sentence (not necessarily MSO), then the right-hand side can be evaluated in $$\Sigma^\mathrm P_k$$.
Since every PH language can be expressed by an SO sentence over finite structures in a suitable signature, we obtain $$\mathrm{PH}=\Sigma^\mathrm P_k$$ if such a collapse holds for all MSO sentences over graphs.