In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using sentences of mathematical logic. There are several variations in the types of logical operation that can be used in these sentences. The first-order logic of graphs concerns sentences in which the variables and predicates concern individual vertices and edges of a graph, while monadic second-order graph logic allows quantification over sets of vertices or edges. Logics based on least fixed point operators allow more general predicates over tuples of vertices, but these predicates can only be constructed through fixed-point operators, restricting their power. A sentence may be true for some graphs, and false for others; a graph is said to model , written , if is true of the vertices and adjacency relation of . The algorithmic problem of model checking concerns testing whether a given graph models a given sentence. The algorithmic problem of satisfiability concerns testing whether there exists a graph that models a given sentence. Although both model checking and satisfiability are hard in general, several major algorithmic meta-theorems show that properties expressed in this way can be tested efficiently for important classes of graphs. Other topics of research in the logic of graphs include investigations of the probability that a random graph has a property specified within a particular type of logic, and methods for data compression based on finding logical sentences that are modeled by a unique graph.
First order
In the first-order logic of graphs, a graph property is expressed as a quantified logical sentence whose variables represent graph vertices, with predicates for equality and adjacency testing.
Examples For instance, the condition that a graph does not have any isolated vertices may be expressed by the sentence
where the symbol indicates the undirected adjacency relation between two vertices. This sentence can be interpreted as meaning that for every vertex there is another vertex that is adjacent to . The subgraph isomorphism problem for a fixed subgraph asks whether appears as a subgraph of a larger graph . It may be expressed by a sentence that states the existence of vertices (one for each vertex of ) such that, for each edge of , the corresponding pair of variables represent adjacent vertices and such that, for each remaining pair of vertices of , the corresponding pair of variables represent distinct vertices; see the illustration. As a special case, the clique problem (for a fixed clique size) may be expressed by a sentence that states the existence of a number of vertices equal to the clique size, all of which are adjacent.
Axioms For simple undirected graphs, the first-order theory of graphs includes the axioms
Other types of graphs, such as directed graphs, may involve different axioms, and logical formulations of multigraph properties require special handling such as having multiple edge relations or separate variables for vertices and edges.
Zero-one law
Glebskiĭ et al. (1969) and, independently, Fagin (1976) proved a zero–one law for first-order graph logic; Fagin's proof used the compactness theorem. According to this result, every first-order sentence is either almost always true or almost always false for random graphs in the Erdős–Rényi model. That is, let be a fixed first-order sentence, and choose a random -vertex graph uniformly at random among all graphs on a set of labeled vertices. Then in the limit as tends to infinity the probability that models will tend either to zero or to one:
Moreover, there is a specific infinite graph, the Rado graph , such that the sentences modeled by the Rado graph are exactly the ones for which the probability of being modeled by a random finite graph tends to one:
For random graphs in which each edge is included independently of the others with a fixed probability, the same result is true, with the same sentences having probabilities tending to zero or to one. The computational complexity of determining whether a given sentence has probability tending to zero or to one is high: the problem is PSPACE-complete. If a first-order graph property has probability tending to one on random graphs, then it is possible to list all the -vertex graphs that model the property, with polynomial delay (as a function of ) per graph. A similar analysis can be performed for non-uniform random graphs, where the probability of including an edge is a function of the number of vertices, and where the decision to include or exclude an edge is made independently with equal probability for all edges. However, for these graphs the situation is more complicated. In this case, a first-order property may have one or more thresholds, such that when the edge inclusion probability is bounded away from the threshold then the probability of having the given property tends to zero or one. These thresholds can never be an irrational power of , so random graphs where the edge inclusion probability is an irrational power obey a zero-one law analogous to the one for uniformly random graphs. A similar zero-one law holds for very sparse random graphs that have an edge inclusion probability of with , as long as is not a superparticular ratio. If is superparticular, the probability of having a given property may tend to a limit that is not zero or one, but this limit can be calculated efficiently. There exist first-order sentences that have infinitely many thresholds.
… excerpt ends here. Continue reading the full article.
