What follows is a description of how to use the compactness theorem from first-order logic to derive a somewhat surprising result. If you're a computer geek and don't care about first-order logic, note that SQL queries are just first-order logic (written in a too-complicated manner). So a database holding links (say, flights between airports) cannot determine accessibility (say, a route -- not even the shortest route!) between two sites without writing procedures. Allowing a stored procedure to run in this case would also be insane -- DFS and BFS are hard! To solve such problems, you'd need a highly denormalized DB.
What is graph theory, first-order logically speaking? The language of graph theory is has the single dyadic (2 place) predicate x~y, that we interpret as "x is adjacent to y". The world of a model of graph theory is the set of nodes of the graph; the predicate "~" gives the edges. A graph is any model G of the 2 axioms
- ∀x.∀y.x~y→y~x ("if x is adjacent to y, then y is adjacent to x")
- ∀x.!(x~x) ("no x is adjacent to itself")
We can express many properties of a graph in the language of first-order logic.
For instance, the property "G contains a triangle" is just the proposition
∃x.∃y.∃z.x~y&y~z&z~x
Similarly, we can translate into first-order logic many nice properties such as "G has
girth k" (for any
given value of
k, there exists a proposition P
k which is true of G
iff G has girth
k), "G has
chromatic number k", and the like.
Are there any properties we cannot express in this way? Graph connectivity is a nice example. Using the compactness theorem we can show that this property cannot be expressed as a proposition of first-order logic.
Suppose the proposition C expressed "G is a connected graph". We will consider graph theory with 2 named points. Add constants s and t to the language ("source" and "sink"). Then C also expressed "G is connected" in the theory of graphs with 2 names points.
For any k, let Lk be the proposition "there is no path of length k between s and t". For instance, proposition L3 is just
!(∃a.∃b. s~a & a~b & b~t)
Now consider the set of propositions Φ = {axiom (i), axiom (ii), C, L1, L2, ...}. Φ is finitely satisfiable: there do exist connected graphs with 2 points (labelled s and t), that are connected by an arbitrarily long path. Since any finite subset F⊂Φ must have bounded k's, such a graph satisifes F.
By the compactness theorem, Φ itself would have to be satisfiable. What does this mean? By Godel's completeness theorem, it means that there exists some model G of all propositions Φ. This model has to be a graph (it satisfies axioms (i) and (ii)); it has to be connected (it satisfies C); and it has 2 nodes s and t, that cannot be connected by a path of length k, for any k (it satisfies all propositions Lk).
This is clearly wrong. In a connected graph, any 2 nodes are connected by a path of finite length! We've just contradicted the possibility of expressing connectivity by a first-order proposition of graph theory.