# Are MSO formulae expressible as existential SO formulae over arbitrary structures?

Given an MSO formulae φ, which may contain arbitrary quantifier alternation, is there always an ESO formula ψ, such that φ and ψ have the same (finite) models?

(This statement holds when the models we are interested in are restricted to words and trees, as one can translate φ to an automaton and back to an MSO formula with an existential quantifier prefix. So the question is really about the general case.)

In MSO one can say that a graph is not $$3$$-colorable: $$\forall C_1 \forall C_2 \forall C_3 (\text{C_1,C_2,C_3 are disjoint sets that cover the graph''} \to \exists x \exists y (E(x,y) \land \bigvee_{i \in \{1,2,3\}} (C_i(x) \land C_i(y)))$$ Since over finite structures ESO is contained in $$NP$$ and non $$3$$-colorability is $$coNP$$-hard, over finite structures non $$3$$-colorability is not definable in ESO unless $$NP = coNP$$. So, probably MSO is not contained in ESO over finite structures.
• @FlorianZuleger I think that MSO $\subseteq$ ESO in the finite is equivalent with NP = coNP. Indeed, if NP = coNP, then PH collapses to NP; in particular, it would follow that in the finite the whole SO is contained in ESO. My answer shows that MSO $\subseteq$ ESO implies in turn that NP = coNP. Commented Jul 6, 2023 at 20:36
An SO formula quantifying over $$k$$-ary relations can be expressed as an MSO formula over a larger structure that includes the $$k$$th cartesian power of the original structure. Thus, up to a polynomial-time blow-up, MSO over arbitrary finite structures can express the whole polynomial hierarchy. (See e.g. Prop. 7.35 in Libkin, Elements of Finite Model Theory, for another argument.)
• It tells you that the answer to the question is negative (assuming NP $\ne$ coNP), because it would imply that every PH language is polynomial-time reducible to an ESO language, and therefore is in NP. Commented Jul 6, 2023 at 15:22