Logic for expressing graph properties

Logic for expressing graph properties --- логика для выражения свойств графа.

Any labelled graph may be defined as a logical structure

[math]\displaystyle{ (V_{G}, E_{G}, (lab_{a,G})_{a \in C_{V}}, (edg_{b,G})_{b \in C_{E}}) }[/math]

where [math]\displaystyle{ V_{G} }[/math] is the set of vertices, [math]\displaystyle{ E_{G} }[/math] is the set of edges, [math]\displaystyle{ C_{V} }[/math] is a set of vertex labels and [math]\displaystyle{ C_{E} }[/math] is a set of edge labels, moreover, the meaning of the predicates is the following:

(1) [math]\displaystyle{ lab_{a,G}(v) }[/math] is true iff the vertex [math]\displaystyle{ v }[/math] has [math]\displaystyle{ a }[/math]-label in [math]\displaystyle{ G }[/math],

(2) [math]\displaystyle{ edg_{b,G}(e,v,v') }[/math] is true iff [math]\displaystyle{ e }[/math] is an edge [math]\displaystyle{ (v,v') }[/math] in [math]\displaystyle{ G }[/math] and has a [math]\displaystyle{ b }[/math]-label in [math]\displaystyle{ G }[/math].

To define the sets of graphs, one considers formulas built by using individual variables (vertex variables or edge variables), set variables (sets of vertices or sets of edges) and binary relation variables (subsets of [math]\displaystyle{ V_{G} \times V_{G} }[/math] or [math]\displaystyle{ V_{G} \times E_{G} }[/math] or [math]\displaystyle{ E_{G} \times E_{G} }[/math]).

Atomic formulas are the following:

(1) [math]\displaystyle{ x = x' }[/math], where [math]\displaystyle{ x,x' }[/math] are two vertices or two edges;

(2) [math]\displaystyle{ lab_{a}(v) }[/math], where [math]\displaystyle{ v }[/math] is a vertex;

(3) [math]\displaystyle{ edg_{b}(e,v,v') }[/math], where [math]\displaystyle{ e }[/math] is an edge and [math]\displaystyle{ v, v' }[/math] are two vertices;

(4) [math]\displaystyle{ x \in X }[/math], where [math]\displaystyle{ X }[/math] is a set of vertices or a set of edges;

(5) [math]\displaystyle{ (x,y) \in R }[/math], where [math]\displaystyle{ R }[/math] is a binary relation included in a cartesian product [math]\displaystyle{ X \times Y }[/math] with [math]\displaystyle{ X }[/math] which is a set of vertices or a set of edges, the same for [math]\displaystyle{ Y }[/math].

A First Order formula is a formula formed with the above atomic formulas numbered from (1) to (3) together with boolean connectives OR, AND, NOT, the individual quantifications [math]\displaystyle{ \forall x, \exists x }[/math] (where [math]\displaystyle{ x }[/math] is a vertex or an edge).

A Monadic Second Order formula is a formula formed with the above atomic formulas numbered from (1) to (4) together with boolean connectives OR, AND, NOT, the individual quantifications [math]\displaystyle{ \forall x, \exists x }[/math] (where [math]\displaystyle{ x }[/math] is a vertex or an edge) and the set quantifications [math]\displaystyle{ \forall X, \exists X }[/math] (where [math]\displaystyle{ X }[/math] is a set of vertices or a set of edges).

A Second Order formula is a formula formed with the above atomic formulas numbered from (1) to (5) together with boolean con\-nec\-tives OR, AND, NOT, the individual quantifications [math]\displaystyle{ \forall x, \exists x }[/math] (where [math]\displaystyle{ x }[/math] is a vertex or an edge), the set quantifications [math]\displaystyle{ \forall X, \exists X }[/math] (where [math]\displaystyle{ X }[/math] is a set of vertices or a set of edges) and the binary relations quantifications [math]\displaystyle{ \forall R, \exists R }[/math] (where [math]\displaystyle{ R }[/math] is a binary relation).