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.