<p>What is the proper definition of MSO<span class="math-container">$_1$</span>?</p>

<p>MSO<span class="math-container">$_1$</span> is also called the one-sorted MSO. In contrast, in MSO<span class="math-container">$_2$</span>, the two-sorted MSO, first order variables and set variables are allowed to be of two sorts -- vertex (set) or edge (set).</p>

<p><strong>Why not define MSO<span class="math-container">$_1$</span> as the fragment of MSO without any edge variables or edge set variable?</strong> (that is, there is only one sort)</p>

<p>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 <span class="math-container">$E(G)$</span> is allowed]. Most authors explicitly state that quantification over <span class="math-container">$E(G)$</span> is allowed. But some authors such as Langer et. al. forbid quantification over <span class="math-container">$E(G)$</span> (see quote below).</p>

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

<p><strong>Details</strong></p>

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

<blockquote>
  <p>Every variable <span class="math-container">$x$</span>, <span class="math-container">$X$</span> is said to have a type tp(<span class="math-container">$x$</span>), tp(<span class="math-container">$X$</span>) <span class="math-container">$\in \{1,2\}$</span> denoting whether it refers to
  vertices (tp(<span class="math-container">$x$</span>) = 1), edges (tp(<span class="math-container">$x$</span>) = 2), vertex sets (tp(<span class="math-container">$X$</span>) = 1),
  or edge sets (tp(<span class="math-container">$X$</span>) = 2), respectively. The formulas of MSO<span class="math-container">$_2$</span> are
  strings that are obtained from finitely many applications of
  the following rules:</p>
  
  <ol>
  <li>If <span class="math-container">$x_1$</span> and <span class="math-container">$x_2$</span> are individual variables with tp(<span class="math-container">$x_1$</span> ) = tp(<span class="math-container">$x_2$</span> ),
  then <span class="math-container">$x_1$</span> = <span class="math-container">$x_2$</span> is a formula.</li>
  <li>If <span class="math-container">$x_1$</span> , <span class="math-container">$x_2$</span> are individual variables with tp(<span class="math-container">$x_1$</span> ) = tp(<span class="math-container">$x_2$</span> ) = 1,
  then adj(<span class="math-container">$x_1$</span> , <span class="math-container">$x_2$</span> ) is a formula.</li>
  <li>If <span class="math-container">$x_1$</span> , <span class="math-container">$x_2$</span> are individual variables with tp(<span class="math-container">$x_1$</span> ) = 1 and
  tp(<span class="math-container">$x_2$</span> ) = 2, then inc(<span class="math-container">$x_1$</span> , <span class="math-container">$x_2$</span> ) is a formula.</li>
  <li>If <span class="math-container">$x$</span> is an individual variable and <span class="math-container">$X$</span> is a set variable with
  tp(<span class="math-container">$x$</span>) = tp(<span class="math-container">$X$</span>), then <span class="math-container">$x\in X$</span> is a formula.</li>
  <li>If <span class="math-container">$\phi$</span> is a formula then <span class="math-container">$\neg\phi$</span> is a formula.</li>
  <li>If <span class="math-container">$\phi_1, \cdots, \phi_k$</span> are formulas then <span class="math-container">$(\phi_1\vee \cdots \vee \phi_k)$</span> and <span class="math-container">$(\phi_1\wedge \cdots \wedge \phi_k)$</span>
  are formulas.</li>
  <li>If <span class="math-container">$\phi$</span> is a formula and <span class="math-container">$x$</span> is an individual variable then <span class="math-container">$\exists x\phi$</span> and <span class="math-container">$\forall x\phi$</span> are formulas.</li>
  <li>If <span class="math-container">$\phi$</span> is a formula and <span class="math-container">$X$</span> is a set variable then <span class="math-container">$\exists X\phi$</span> and <span class="math-container">$\forall X\phi$</span> are formulas.</li>
  </ol>
  
  <p>If the formulas in 8 use edge set variables (tp(<span class="math-container">$X$</span>) = 2), we
  call this quantification an edge set quantification. .......... MSO without
  quantification over sets of edges, i.e., with <strong>quantification over
  sets of vertices only is called MSO<span class="math-container">$_1$</span></strong> or one-sorted MSO.</p>
</blockquote>

CC BY-SA 4.0
2019-07-04T08:18:22.783Z
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.
Gamow
CC BY-SA 4.0
2019-07-04T08:27:45.293Z
@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.
Cyriac Antony
CC BY-SA 4.0
2019-07-04T11:43:15.410Z
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.
Emil Jeřábek
CC BY-SA 4.0
2019-07-04T12:43:19.113Z
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.
Emil Jeřábek
<model-checking>
Definition of MSO_1 for graph structures
Cyriac Antony
# Definition of MSO_1 for graph structures

(Asked by: username_0 on 2019-07-04)

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.

**Tags:** model-checking

> **Comments:**
> **username_1**: 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.  
> **username_0**: @username_1 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.  
> **username_2**: 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.  
> **username_2**: 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.  

---

## 0 answers

