Is graph connectivity definable in existential MSO with vertices and edges?

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.

• 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. Aug 25 '18 at 17:27
• Ah, thanks @Emil, that sounds like a more sensible interpretation. Aug 25 '18 at 17:48

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).
• 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$. Aug 27 '18 at 6:00
• @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. Aug 27 '18 at 7:58