<p>If I understand correctly, you just want a definition of the logic; then you can find a definition of MSO$_j$ (where 2 is a special case) by example in ''Elements of Finite Model Theory'' of Leonid Libkin.
Even if you are interested in infinite model, the definition of the logic is the same.</p>

<p>Quickly is just the set of formulae with existantial quantification over sets of the elements of the universe, then existantial quantifications over those sets; then a first-order formula.</p>

CC BY-SA 2.5
2010-08-30T14:48:43.497Z
Thanks for the answer. The definition for MSO in "Elements of Finite Model Theory" is what I mean with MSO1. For graphs MSO2 is MSO over the incidence graph. This allows to quantify over sets of edges. However I don't really see how this generalizes to arbitrary structures.
Martin Lackner
CC BY-SA 2.5
2010-08-29T02:13:22.783Z
2010-08-29T02:13:22.783Z
Arthur MILCHIOR
<p>You can also use <em>many-sorted</em> second order logic which allows quantification over sets of each sort. </p>

<p>Example: graphs, use two sorts, one for vertices and one for edges.</p>

CC BY-SA 4.0
2019-05-29T12:23:58.127Z
For the record, nowadays this definition is considered is the "usual" definition
Cyriac Antony
CC BY-SA 2.5
2010-08-30T14:54:50.167Z
Thanks for your answer. This sounds like it is close to what I am looking for. However I am not really interested in a new definition for MSO2, but would like to cite the "usual" definition.
Martin Lackner
CC BY-SA 2.5
2010-08-29T04:50:40.760Z
2010-08-29T04:50:40.760Z
Kaveh
<p>Have a look at page 75 in the <a href="http://www.labri.fr/perso/courcell/Book/TheBook.pdf" rel="nofollow">draft of the book by Courcelle and Engelfriet</a>. </p>

CC BY-SA 3.0
2016-07-01T05:31:54.917Z
2016-07-01T05:31:54.917Z
f-h
<p>I am not able to find a rigorous definition of MSO_2 logic for arbitrary structures (which I can cite). MSO_2 for graphs is often used and defined, i.e. in On the Parameterised Intractability of Monadic Second-Order Logic - Stephan Kreutzer. The only "definition" for MSO2 on structures I found was in A logical approach to multicut problems - Gottlob, Lee.</p>

<p>"The definition of MSO2 can be easily
generalized to arbitrary structures by allowing quantifi-
cation over subsets of the input relation (notice that in
the case of a graph, the input relation is just the edge re-
lation). Thus, for example, if a relational symbol R is
part of the signature, then a subformula (∃X ⊆ R)φ(X),
expressing that there exists a subset X of the relation R
such that φ(X) holds for some formula φ, could be part
of an MSO2 formula."</p>

<p>While this is enough explanation to know what MSO2 on arbitrary structures is, I really would appreciate if someone could give me a pointer to a formal, rigorous definition somewhere in the literature.</p>

<lo.logic>
Definition for MSO2 for arbitrary structures
Martin Lackner
# Definition for MSO2 for arbitrary structures

(Asked by: username_0 on 2010-08-28)

I am not able to find a rigorous definition of MSO\_2 logic for arbitrary structures (which I can cite). MSO\_2 for graphs is often used and defined, i.e. in On the Parameterised Intractability of Monadic Second-Order Logic - Stephan Kreutzer. The only "definition" for MSO2 on structures I found was in A logical approach to multicut problems - Gottlob, Lee.

"The definition of MSO2 can be easily
generalized to arbitrary structures by allowing quantifi-
cation over subsets of the input relation (notice that in
the case of a graph, the input relation is just the edge re-
lation). Thus, for example, if a relational symbol R is
part of the signature, then a subformula (∃X ⊆ R)φ(X),
expressing that there exists a subset X of the relation R
such that φ(X) holds for some formula φ, could be part
of an MSO2 formula."

While this is enough explanation to know what MSO2 on arbitrary structures is, I really would appreciate if someone could give me a pointer to a formal, rigorous definition somewhere in the literature.

**Tags:** lo.logic

---

## 3 answers

### Answer by username_1 on 2010-08-29. Score: 5

If I understand correctly, you just want a definition of the logic; then you can find a definition of MSO$\_j$ (where 2 is a special case) by example in ''Elements of Finite Model Theory'' of Leonid Libkin.
Even if you are interested in infinite model, the definition of the logic is the same.

Quickly is just the set of formulae with existantial quantification over sets of the elements of the universe, then existantial quantifications over those sets; then a first-order formula.

> **Comments:**
> **username_0**: Thanks for the answer. The definition for MSO in "Elements of Finite Model Theory" is what I mean with MSO1. For graphs MSO2 is MSO over the incidence graph. This allows to quantify over sets of edges. However I don't really see how this generalizes to arbitrary structures.  

---

### Answer by username_2 on 2010-08-29. Score: 5

You can also use *many-sorted* second order logic which allows quantification over sets of each sort.

Example: graphs, use two sorts, one for vertices and one for edges.

> **Comments:**
> **username_0**: Thanks for your answer. This sounds like it is close to what I am looking for. However I am not really interested in a new definition for MSO2, but would like to cite the "usual" definition.  
> **username_3**: For the record, nowadays this definition is considered is the "usual" definition  

---

### Answer by username_4 on 2016-07-01. Score: 0

Have a look at page 75 in the [draft of the book by Courcelle and Engelfriet](http://www.labri.fr/perso/courcell/Book/TheBook.pdf).


---

