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

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

Now consider the set of propositions Φ = {axiom (i), axiom (ii), C, L_{1}, L_{2}, ...}. Φ 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.