MSO2-expressible graph properties unexpressible in MSO1 I would like to ask if there is any good list of graph properties that one can express in the MSO2 (i.e., using quantification over sets of edges) but provably not in MSO1 (i.e., using quantification over sets of vertices only). I know that this should be Hamilton path but I think that there has to be plenty such examples. Ideal are those that are suitable as exercises for non-expressibility results using Ehrenfeucht–Fraïssé games.
 A: Nice question.  I am also keen to learn of more examples.  
Here are some more details on the Hamiltonian cycle example.  This is expressible in $\mathsf{MSO_2}$ since testing if a graph is connected is expressible in $\mathsf{MSO}_2$ and testing if a set of edges induces a $2$-regular subgraph is clearly expressible in $\mathsf{MSO}_2$.  Indeed, connectivity is actually expressible in $\mathsf{MSO_1}$ since a graph $G$ is connected if and only if for all partitions $A \cup B$ of $V(G)$ there is an edge between $A$ and $B$.  However, $\mathsf{MSO}_1$ does not know the difference between balanced complete bipartite graphs (which do have Hamiltonian cycles) and unbalanced complete bipartite graphs (which do not have Hamiltonian cycles).  
Edit.  Another example I thought that works is the existence of an odd (or even) length path between two fixed vertices $u$ and $v$.  However, this turns out to be expressible in both $\mathsf{MSO}_2$ and $\mathsf{MSO}_1$. Thanks to Emil Jeřábek for the comments below.  
Odd length paths are expressible in $\mathsf{MSO}_2$ since a path between $u$ and $v$ is a set of edges $P$ such that $G[P]$ is connected, $u$ and $v$ have degree $1$ in $G[P]$ and all other vertices in $G[P]$ have degree $2$.  We can say that $P$ has odd length in $\mathsf{MSO}_2$ since $P$ has odd length (length is the number of edges) if and only if there exists a partition $A \cup B$ of $V(P)$ such that $u \in A$, $v \in B$, and for each $e \in P$, $e$ has one end in $A$ and one end in $B$. 
For $\mathsf{MSO}_1$, we can say that $u$ and $v$ are connected by an odd length path in $G$ if there exist disjoint subsets $A$ and $B$ of $V(G)$ such that $u \in A$, $v \in B$, and the subgraph consisting of all edges between $A$ and $B$ is connected.  
A: I have found a book available online which gives some answers to your question. The book is Graph Structure and Monadic Second-Order Logic: a Language Theoretic Approach by Courcelle and Engelfriet. I am not (at all) an expert on this topic, but the book seems like a good reference. It lists the existence of a Hamiltonian cycle as an example. Some additional interesting examples included in the book are:


*

*If a graph is simple

*Existence of a perfect matching

*Existence of a spanning tree with maximum degree 3


The most relevant parts of the book are Proposition 5.13, Proposition 5.19, and Remark 5.21. Showing the existence of a perfect matching is not expressible in $MSO_1$ can be with the same arguement on complete bipartite graphs $K_{n,m}$ outlined in Tony Huynh's answer. Also, it seems to me the example of a spanning tree with maximum degree 3 in Remark 5.21 can be modified to show that the existence of a spanning tree with maximum degree $k$ for some given $k$ in not expressible in $MSO_1$ (put more "leaves" on the graph in Figure 5.3).
