Example 2. The class of simple graphs is the class of structures over G1 =
(u; Adj(u; u); ) defined by: 8x8y Adj(x; y) $ Adj(y; x). This formula says that
the adjacency relation Adj must be symmetric in a graph. Similarly, the class of
directed multi-graphs can be defined in a two-sorted signature,
G2 = (u; v; It(u; v); Ih(u; v); ) with sort 'edge' u and 'vertex' v, using the head and tail incidence relations Ih(u; v) and It(u; v) and the conditions: "Every edge is the tail of exactly one vertex and the head of exactly one vertex". This condition can, somewhat tediously, be defined in first-order logic with equality. But the condition could also be built into the signature by regarding tail and head as two functions from edge to vertex.
The second order logic is obtained from first order logic by adding variables of a new kind denoting relations or functions of a known profile and quantification over such variables. These variables can be used as the corresponding constants in atoms and terms. The satisfaction relation of first order logic is augmented so that in an assignment, a relation or function table of the right profile is assigned to a second order variable. It turns out that full second order logic is too general for our main purpose here. The monadic second order logic is the restricted logic where second order variables can only be unary relation variables, which naturally denote sets from the domain. In monadic second order logic we use set variables for unary relation variables and the set inclusion operator ae and the membership operator 2. Thus, x 2 Y is used for what in second order logic would be Y (x). We define a monadic second order definable set of structures L to be the set of structures satisfying some monadic second order formula OE, L = fI j I j= OEg.
For a formula with free variables, and for a compatible structure, satisfaction depends on a variable assignment. The set of satisfying assignments of a formula ' with respect to a structure I is the set of variable assignments for which I satisfies ', fV j I j= '[V ]g. If we have ordered the m free variables, we can represent the satisfying assignments as m-tuples, with one component for each free variable of ' (it is not difficult to see that satisfaction depends only on the assignment to the free variables). Such a set of m-tuples is called a monadic second order definable set of tuples in a structure.
It was shown by Courcelle that it is not possible to 'do counting' in
monadic second order logic, i.e., it is not possible to express conditions like: 'set
X has more elements than set Y ' or 'set X has an odd number of elements'.
Following Courcelle we add to monadic second order logic the modular counting
relation constants Modr;p for p = 2; 3; : : : and r = ; : : : ; p ? 1. The meaning of
Modr;p(X) is: 'the size of X modulo p is r'. This extended logic is called S logic. Similarly, S-definable families of structures and S definable sets of tuples are obtained by just adding modular counting to the corresponding definitions for monadic second order logic.
1.2 Interpretation of structures in structures.
Interpretation is a method for defining a map from structures over one signature F to structures over another signature F . We present here an extension