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