<p>You can express that $s$ is connected to $t\ne s$ in $G=(V,E)$ by the $\exists\mathrm{MSO}_2$ formula</p>

<blockquote>
  <p>“there exists $E'\subseteq E$ such that in the graph $(V,E')$, $s$ and $t$ have degree $1$, and all other vertices have degree $0$ or $2$.”</p>
</blockquote>

<p>Note that the formula after the initial $\exists E'$ quantifier is first-order.</p>

<p>A graph of degree $\le2$ is a disjoint union of lines and cycles; since end-points of lines are exactly the vertices of degree $1$, the only way to satisfy the formula is that $E'$ consists of a line connecting $s$ to $t$, and possibly some disjoint cycles.</p>

<p>Likewise, directed connectivity can also be defined by an $\exists\mathrm{MSO}_2$ formula (we replace “degree $2$” with “in-degree and out-degree $1$”, and similarly for the end-points).</p>

CC BY-SA 4.0
2018-08-27T06:00:51.930Z
Curiously, this formula works only for finite graphs. An infinite graph can have such a set $E'$ and still fail to connect $s$ to $t$.
David Eppstein
CC BY-SA 4.0
2018-08-27T07:58:03.167Z
@DavidEppstein Right. And there is no way around it; it follows easily from compactness that if a $\Sigma^1_1$ formula implies connectedness on arbitrary graphs, it implies connectedness by paths of bounded length.
Emil Jeřábek
CC BY-SA 4.0
2024-04-03T14:49:38.630Z
This expresses $(s,t)$-connectivity, not graph connectivity. One could add $\forall s, t$ in front of it, but that would not be $\exists MSO_2$. Is there another way to express graph connectivity not using the $\forall$ quantifiers?
J. Schmidt
CC BY-SA 4.0
2024-04-04T08:59:57.583Z
@J.Schmidt Yes, this is $s$-$t$-connectivity, which is the problem specifically formulated near the end of the question. I do not know if you can express by an $\exists\mathrm{MSO_2}$ sentence that the whole graph is connected; it sounds unlikely.
Emil Jeřábek
CC BY-SA 4.0
2018-08-26T11:23:59.453Z
2018-08-26T11:23:59.453Z
Emil Jeřábek
<blockquote>
  <p>Can $\exists$MSO$_2$ express graph connectivity?</p>
</blockquote>

<p>Monadic SO (MSO) is the fragment of second-order logic in which the second-order quantifiers range over relations of arity 1 only.
$\exists$MSO is the fragment of MSO in which only non-negated existential second-order quantification is allowed.</p>

<p>MSO over graphs (sometimes denoted MSO$_1$) has as its universe vertices only.
In contrast, the variant MSO$_2$ has as its universe vertices as well as edges.</p>

<p>It is well-known that MSO$_2$ is more expressive than MSO$_1$; for instance, the former can express the existence of a Hamiltonian cycle (see Libkin's <em>Elements of Finite Model Theory</em>, Exercise 7.4), while the latter cannot (Libkin's proof of Corollary 7.24 is a neat pumping argument due to Makowsky).</p>

<p>It is also standard that $\exists$MSO$_1$ cannot express graph connectivity.  One proof is via Hanf locality due to Fagin, Stockmeyer, and Vardi (Information and Computation 1995).  This paper states: "we consider it possible that connectivity is not in monadic NP, even in the presence of arbitrary built-in relations of arbitrary degree"<strike>; the edge relation has arity 2 so they are conjecturing that the answer to my question is negative</strike> (monadic NP is the same as $\exists$MSO).
<em>(Removed last clause as per comment of Emil Jeřábek.)</em></p>

<p>More recently, Courcelle and Engelfriet's textbook on MSO mentions that it is possible to express "$X$ is a set of edges forming a directed path from $s$ to $t$" in MSO$_2$.  However, their formula uses universal quantification.  It is not immediately obvious whether this is necessary, at least for the concept of connectivity of an undirected graph.</p>

CC BY-SA 4.0
2018-08-25T17:27:32.670Z
I think "built-in relation" refers here to relations that are fixed once and for all on the base set, such as the + and × in FO(+,×). They cannot depend on the graph. Otherwise the claim would be obviously false, as you could just directly add the binary relation of connectivity, making it quantifier-free definable.
Emil Jeřábek
CC BY-SA 4.0
2018-08-25T17:48:14.130Z
Ah, thanks @Emil, that sounds like a more sensible interpretation.
András Salamon
<graph-theory><lo.logic><finite-model-theory>
Is graph connectivity definable in existential MSO with vertices and edges?
András Salamon
# Is graph connectivity definable in existential MSO with vertices and edges?

(Asked by: username_0 on 2018-08-25)

> Can $\exists$MSO$\_2$ express graph connectivity?

Monadic SO (MSO) is the fragment of second-order logic in which the second-order quantifiers range over relations of arity 1 only.
$\exists$MSO is the fragment of MSO in which only non-negated existential second-order quantification is allowed.

MSO over graphs (sometimes denoted MSO$\_1$) has as its universe vertices only.
In contrast, the variant MSO$\_2$ has as its universe vertices as well as edges.

It is well-known that MSO$\_2$ is more expressive than MSO$\_1$; for instance, the former can express the existence of a Hamiltonian cycle (see Libkin's *Elements of Finite Model Theory*, Exercise 7.4), while the latter cannot (Libkin's proof of Corollary 7.24 is a neat pumping argument due to Makowsky).

It is also standard that $\exists$MSO$\_1$ cannot express graph connectivity. One proof is via Hanf locality due to Fagin, Stockmeyer, and Vardi (Information and Computation 1995). This paper states: "we consider it possible that connectivity is not in monadic NP, even in the presence of arbitrary built-in relations of arbitrary degree"; the edge relation has arity 2 so they are conjecturing that the answer to my question is negative (monadic NP is the same as $\exists$MSO).
*(Removed last clause as per comment of Emil Jeřábek.)*

More recently, Courcelle and Engelfriet's textbook on MSO mentions that it is possible to express "$X$ is a set of edges forming a directed path from $s$ to $t$" in MSO$\_2$. However, their formula uses universal quantification. It is not immediately obvious whether this is necessary, at least for the concept of connectivity of an undirected graph.

**Tags:** graph-theory, lo.logic, finite-model-theory
> **Comments:**
> **username_1**: I think "built-in relation" refers here to relations that are fixed once and for all on the base set, such as the + and × in FO(+,×). They cannot depend on the graph. Otherwise the claim would be obviously false, as you could just directly add the binary relation of connectivity, making it quantifier-free definable.  
> **username_0**: Ah, thanks @Emil, that sounds like a more sensible interpretation.  

---

## 1 answers

### Answer by username_1 on 2018-08-26. Score: 9 | Accepted answer

You can express that $s$ is connected to $t\ne s$ in $G=(V,E)$ by the $\exists\mathrm{MSO}\_2$ formula

> “there exists $E'\subseteq E$ such that in the graph $(V,E')$, $s$ and $t$ have degree $1$, and all other vertices have degree $0$ or $2$.”

Note that the formula after the initial $\exists E'$ quantifier is first-order.

A graph of degree $\le2$ is a disjoint union of lines and cycles; since end-points of lines are exactly the vertices of degree $1$, the only way to satisfy the formula is that $E'$ consists of a line connecting $s$ to $t$, and possibly some disjoint cycles.

Likewise, directed connectivity can also be defined by an $\exists\mathrm{MSO}\_2$ formula (we replace “degree $2$” with “in-degree and out-degree $1$”, and similarly for the end-points).

> **Comments:**
> **username_2**: Curiously, this formula works only for finite graphs. An infinite graph can have such a set $E'$ and still fail to connect $s$ to $t$.  
> **username_1**: @DavidEppstein Right. And there is no way around it; it follows easily from compactness that if a $\Sigma^1_1$ formula implies connectedness on arbitrary graphs, it implies connectedness by paths of bounded length.  
> **username_3**: This expresses $(s,t)$-connectivity, not graph connectivity. One could add $\forall s, t$ in front of it, but that would not be $\exists MSO_2$. Is there another way to express graph connectivity not using the $\forall$ quantifiers?  
> **username_1**: @J.Schmidt Yes, this is $s$-$t$-connectivity, which is the problem specifically formulated near the end of the question. I do not know if you can express by an $\exists\mathrm{MSO_2}$ sentence that the whole graph is connected; it sounds unlikely.  

---

