Definition for MSO2 for arbitrary structures

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

Have a look at page 75 in the draft of the book by Courcelle and Engelfriet.