# Definition of MSO_1 for graph structures

What is the proper definition of MSO$$_1$$?

MSO$$_1$$ is also called the one-sorted MSO. In contrast, in MSO$$_2$$, the two-sorted MSO, first order variables and set variables are allowed to be of two sorts -- vertex (set) or edge (set).

Why not define MSO$$_1$$ as the fragment of MSO without any edge variables or edge set variable? (that is, there is only one sort)

Instead, it is usually defined as the fragment of MSO without edge set quantification [some authors say quantification over sets of edges; it is ambiguous whether quantification over $$E(G)$$ is allowed]. Most authors explicitly state that quantification over $$E(G)$$ is allowed. But some authors such as Langer et. al. forbid quantification over $$E(G)$$ (see quote below).

I think my definition and the definition by Langer are actually same because we can express edge variables by vertex sets instead (eg: $$\exists S\ \exists a\ \exists b\ ( a\neq b \wedge \forall c (c\in S\implies c=a \vee c=b) )$$. Or am I mistaken?

Details

Here is a quote from Practical algorithms for MSO model-checking on tree-decomposable graphs by Langer et. al. (emphasis mine)

Every variable $$x$$, $$X$$ is said to have a type tp($$x$$), tp($$X$$) $$\in \{1,2\}$$ denoting whether it refers to vertices (tp($$x$$) = 1), edges (tp($$x$$) = 2), vertex sets (tp($$X$$) = 1), or edge sets (tp($$X$$) = 2), respectively. The formulas of MSO$$_2$$ are strings that are obtained from finitely many applications of the following rules:

1. If $$x_1$$ and $$x_2$$ are individual variables with tp($$x_1$$ ) = tp($$x_2$$ ), then $$x_1$$ = $$x_2$$ is a formula.
2. If $$x_1$$ , $$x_2$$ are individual variables with tp($$x_1$$ ) = tp($$x_2$$ ) = 1, then adj($$x_1$$ , $$x_2$$ ) is a formula.
3. If $$x_1$$ , $$x_2$$ are individual variables with tp($$x_1$$ ) = 1 and tp($$x_2$$ ) = 2, then inc($$x_1$$ , $$x_2$$ ) is a formula.
4. If $$x$$ is an individual variable and $$X$$ is a set variable with tp($$x$$) = tp($$X$$), then $$x\in X$$ is a formula.
5. If $$\phi$$ is a formula then $$\neg\phi$$ is a formula.
6. If $$\phi_1, \cdots, \phi_k$$ are formulas then $$(\phi_1\vee \cdots \vee \phi_k)$$ and $$(\phi_1\wedge \cdots \wedge \phi_k)$$ are formulas.
7. If $$\phi$$ is a formula and $$x$$ is an individual variable then $$\exists x\phi$$ and $$\forall x\phi$$ are formulas.
8. If $$\phi$$ is a formula and $$X$$ is a set variable then $$\exists X\phi$$ and $$\forall X\phi$$ are formulas.

If the formulas in 8 use edge set variables (tp($$X$$) = 2), we call this quantification an edge set quantification. .......... MSO without quantification over sets of edges, i.e., with quantification over sets of vertices only is called MSO$$_1$$ or one-sorted MSO.

• What is "Langer et al"? The standard reference for this area is the book "Graph Structure and Monadic Second-Order Logic, a Language Theoretic Approach" by Bruno Courcelle and Joost Engelfriet. Jul 4 '19 at 8:18
• @Gamow I know. Practical algorithms for MSO model-checking on tree-decomposable graphs by Langer et. al. is a recent survey which is more approachable for people like me without a good background in language theory. I couldn't find such a short definition in the book. Jul 4 '19 at 8:27
• Even simpler, you can simulate a quantifier over $E(G)$ by two quantifiers over $V(G)$. I guess the choice whether to include a first-order sort for $E(G)$ is just a matter of convenience. Jul 4 '19 at 11:43
• I should add that the two approaches are equivalent for simple graphs. If you study graphs that may have multiple edges, then an $E(G)$ sort becomes indispensable. Jul 4 '19 at 12:43