This is an old revision of the document!
Graphs as Interpretations
Directed graph is given by a set of vertices and a set of edges . Graph is therefore specified by an interpretation in languge with .
Example: , .
For a class of graph properties we can write down a formula such that property holds for graph iff is true in the interpretation representing the graph.
No self-loops: \[
\forall x.\ \lnot edge(x,x)
Undirected graph: \[
\forall x.\ edge(x,y) \rightarrow edge(y,x)
\forall x, y.\ (edge(x,y) \lor edge(y,x)) \land \lnot (edge(x,y) \land edge(y,x))
Note: there is no formula in this language that characterizes property “graph has no cycles”. All properties expressed in first-order logic on graphs are “local”. Intuitively, formula with universal quantifiers says that if we pick any set of vertices in the graph, then they (and their close neighbors) can induce only one of the finitely many specified subgraphs.
Many more properties become expressible if we take as domain the set of all subsets of and allow set operations in our language.