Graph theory in first-order logic

Question

I state that I'm not very experienced in mathematical logic. I read that the theory of graphs in first-order logic is formalized simply by means of a binary predicate $R(x, y)$ which express the fact that two vertices are connected by an edge. Then one can impose some axioms to $R(x, y)$ for example that it is an irreflexive and symmetric relation.

My question is: if I want to add some information to the edges, for example, a weight, I need to reify edges in the domain of discourse in such a way that it is possible to quantify over and inscribe to the properties. Is it correct? (I want to remain in a first-order logic).

What I have in mind is to use two unary predicates, say $E(x)$ for $x$ is an edge and $V(x)$ for $x$ is a vertex, and one of the following relation:

• a ternary relation $C(x, y, z)$ to say that the edge $y$ connects the vertices $x$ and $z$

or

• two binary relations $R_1(x, y)$ and $R_2(y, w)$ (appropriately axiomatized) to say that the vertices $x$ and $w$ are connected through the edge $y$

Could you tell me if there are some books or papers which explain such things?

Thanks

Answer 1

Try the lovely paper:

Cai-Furer-Immerman "An Optimal Lower Bound on the Number of Variables for Graph Identification".

Not only does it set up in a very gentle way the methods of encoding graph theory in first order logic (including with labels and all), but it then goes on to prove remarkable properties such as that you can make graphs that are non-isomorphic but cannot be distinguished by any k-ary relations until $k\approx n$ (sometimes those methods are called "color refinement" or Weisefieler-Lehman invariants). I used that paper in a intro grad seminar and the students seemed to follow it well so I guage that as external validation to my own view of its excellent writing.

If that doesn't suite try "The graph isomorphism problem -- Its structural complexity" by Kobler-Schoening-Toran

Answer 2

Both of your approaches seem sensible. In fact, why not use both kinds of predicates, as depending on what you are trying to do or prove, using one set of predicates may be more helpful than the other set.

I think I would use $C(x,y,z)$ as '$x$ is an edge connecting vertices $y$ and $z$', so that the order of the arguments corresponds with the order of the arguments as they occur in a natural English expression of that statement.

To express irreflexivity, you can then do:

$$\forall x \forall y \neg C(x,y,y)$$

For symmetry:

$$\forall x \forall y \forall z (C(x,y,z) \leftrightarrow C(x,z,y))$$

Also, if you are using undirected graphs, you can just use a single predicate $R(x,y)$ to express that '$x$ is an edge connected to vertex $y$'.

And you can use the following as an axiom to go between the different predicates:

$$\forall x \forall y \forall z ((E(x) \land V(y) \land V(z)) \rightarrow (C(x,y,z) \leftrightarrow (R(x,y) \land R(x,z)))$$

Also useful might be:

$$\forall x \forall y ((E(x) \land V(y)) \rightarrow ((C(x,y,z) \land R(x,y)) \rightarrow \exists z (V(z) \land R(x,z))))$$

If you have directed graphs, maybe use $From(x,y)$ and $To(x,y)$ as 'edge $x$ goes from vertex $y$' and 'edge $x$ goes to vertex $y$' respectively. And you can easily modify the above axioms to deal with those.