5
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Aug 25, 2018 at 17:27
  • $\begingroup$ Ah, thanks @Emil, that sounds like a more sensible interpretation. $\endgroup$
    – András Salamon
    Aug 25, 2018 at 17:48

1 Answer 1

Reset to default
9
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ 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$. $\endgroup$
    – David Eppstein
    Aug 27, 2018 at 6:00
  • 2
    $\begingroup$ @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. $\endgroup$
    – Emil Jeřábek
    Aug 27, 2018 at 7:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.