<p>In MSO one can say that a graph is <em>not</em> <span class="math-container">$3$</span>-colorable:
<span class="math-container">$$\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)))$$</span>
Since over finite structures ESO is contained in <span class="math-container">$NP$</span> and non <span class="math-container">$3$</span>-colorability is <span class="math-container">$coNP$</span>-hard, over finite structures non <span class="math-container">$3$</span>-colorability is not definable in ESO unless <span class="math-container">$NP = coNP$</span>. So, probably MSO is not contained in ESO over finite structures.</p>
<p>MSO is also not contained in ESO over general structures. For instance, in MSO one can axiomatize the standard structure of real numbers up to isomorphism (which is an uncountable structure) while every ESO sentence that has an infinite model has a countably infinite model (due to the fact that ESO has the countable downwards Löwenheim-Skolem property).</p>

CC BY-SA 4.0
2023-07-06T15:01:46.787Z
Thanks! The second argument separates MSO and ESO for infinite structures. It would still be nice to find an argument for finite structures that does not rely on NP ≠ coNP.
Florian Zuleger
CC BY-SA 4.0
2023-07-06T20:36:33.620Z
@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.
Reijo Jaakkola
CC BY-SA 4.0
2023-07-05T09:49:45.393Z
2023-07-05T09:49:45.393Z
Reijo Jaakkola
<p>An SO formula quantifying over <span class="math-container">$k$</span>-ary relations can be expressed as an MSO formula over a larger structure that includes the <span class="math-container">$k$</span>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, <a href="https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf" rel="nofollow noreferrer">Elements of Finite Model Theory</a>, for another argument.)</p>

CC BY-SA 4.0
2023-07-06T15:05:43.783Z
As the approach you suggest requires changing the structure it does not help my question where I am interested in finding an ESO formula ψ that has the same models as a given MSO formula φ.
Florian Zuleger
CC BY-SA 4.0
2023-07-06T15:22:21.970Z
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.
Emil Jeřábek
CC BY-SA 4.0
2023-07-05T09:54:46.353Z
2023-07-11T08:37:42.063Z
2023-07-11T08:37:42.063Z
Emil Jeřábek
<p>Given an MSO formulae φ, which may contain arbitrary quantifier alternation, is there always an ESO formula ψ, such that φ and ψ have the same (finite) models?</p>
<p>(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.)</p>

<lo.logic><model-theory>
Are MSO formulae expressible as existential SO formulae over arbitrary structures?
Florian Zuleger
# Are MSO formulae expressible as existential SO formulae over arbitrary structures?

(Asked by: username_0 on 2023-07-05)

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.)

**Tags:** lo.logic, model-theory

---

## 2 answers

### Answer by username_1 on 2023-07-05. Score: 7

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.

MSO is also not contained in ESO over general structures. For instance, in MSO one can axiomatize the standard structure of real numbers up to isomorphism (which is an uncountable structure) while every ESO sentence that has an infinite model has a countably infinite model (due to the fact that ESO has the countable downwards Löwenheim-Skolem property).

> **Comments:**
> **username_0**: Thanks! The second argument separates MSO and ESO for infinite structures. It would still be nice to find an argument for finite structures that does not rely on NP ≠ coNP.  
> **username_1**: @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.  

---

### Answer by username_2 on 2023-07-05. Score: 4

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](https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf), for another argument.)

> **Comments:**
> **username_0**: As the approach you suggest requires changing the structure it does not help my question where I am interested in finding an ESO formula ψ that has the same models as a given MSO formula φ.  
> **username_2**: 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.  

---

