Connectivity is not expressible in first-order logic

(Mathematical logic, graph theory)

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

1. ∀x.∀y.x~y→y~x ("if x is adjacent to y, then y is adjacent to x")
2. ∀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

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.

Proof.

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 L_k be the proposition "there is no path of length k between s and t". For instance, proposition L₃ is just

!(∃a.∃b. s~a & a~b & b~t)

Now consider the set of propositions Φ = {axiom (i), axiom (ii), C, L₁, L₂, ...}. Φ 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 L_k).

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.