Favorite Logic of September 2005: First-order Logic (3)

previous|
next

We are somewhat behind our schedule. So, let's close it out now. This post concludes our series of posts on first-order logic as the favorite logic of last month (oops!). I will give a glimpse of the expressiveness of first-order logic, and tools for showing inexpressibility results. The literature on this topic is so vast that it is impossible to cover all possible results and tools; so, I will mention only a selection of results and tools, and give examples on how to apply the tools mentioned. Also, see the preliminaries before reading this post.

Let's get right down to business. Our main problem can be described as follows: suppose Q is a σ-property (i.e. boolean query), and we want to know whether there exists a first-order sentence that defines Q. If there is one, then it suffices to come up with a sentence f that defines Q. If not, what shall we do?

Well ... in model theory, we have a plethora of tools in our toolbox:

1. Compactness: a theory T is consistent iff every finite subset of T is consistent.
   
2. (Restricted form of) Lowenheim-Skolem: If a theory has an infinite model, then it has a countable model.
   

Let's try compactness on an example. Suppose we want to show that the property GC testing graph connectivity is not first-order definable. Suppose to the contrary that f defines GC. Then, consider the theory T = {f} ∪ { π_n : n is positive nat. number } where π_n is the first-order sentence

∃x∃y( there is no path of length n from x to y )

Clearly, this sentence is first-order. By compactness, it is easy to show that T is consistent (just take the biggest n for which π_n appears in this finite subset of T and "elongate" the path from x to y by increasing the number of elements in the universe). So, we have a model M for T. But in M, x and y are not connected by a (finite) path, contradicting f. Therefore, f cannot be a first-order sentence.

That's short and simple! The problem, however, is that this doesn't prove that FO cannot express GC in the finite (i.e. the ground set of GC is restricted to all finite graphs only), as compactness theorem fails in the finite. So, how do we prove that GC cannot be expressed in the finite? It is a sad fact that most of the tools from model theory fails in the finite. Some of the few that survive include Ehrenfeucht-Fraisse game theorem, Gaifmann-locality, and Hanf-locality. Here we shall use the notion of Hanf-locality to prove that GC is not FO definable.

Let me try to intuitively illustrate the notion of Hanf-locality for graphs. A graph property P (over all finite structures) is said to be hanf-local if there exists a number d such that for every two finite graphs A and B:

that A and B d-locally look the same implies that A and B agree on P.

The smallest such number d is called hanf-locality rank of P. What do we mean by "d-locally look the same"? A and B d-locally look the same if there exists a bijection g from V(A) to V(B), the vertices of A and B, such that for every c in V(A) there exists an isomorphism from the d-neighborhood of A around c to the d-neighborhood of B around g(c) which maps c to g(c). That is, if you have only limited local vision (say up to d distance) and if you pick a spot c in the graph A, I can always give you another spot in the graph B (via the bijection) such that you cannot see the difference between your surroundings on these two different spots.

Now, our strategy for proving that GC is not first-order expressible is:

1. Show that every first-order definable query is hanf-local.
   
2. Show that GC is not hanf-local.
   

We won't prove item 1. We will however sketch how to prove item 2. Suppose GC is hanf-local with rank d. Then, define two graphs G and G' as follows. Take a number p >> d. G is a cycle with 2p nodes, and G' is a disjoint union of cycles each with p nodes. You can easily check that there is only one type of d-neighborhood (up to isomorphism) around any vertex c in G and G', i.e., the 2d+1-path with c right in the middle. So, just take any arbitrary bijection between G and G' to show that they d-locally look the same. However, G is connected but G' is not, contradicting the assumption that GC is hanf-local!

I would love to talk about Ehrenfeucht-Fraisse games and Gaifmann locality, which are equally important tools in finite model theory for proving FO inexpressibility. Sadly, this will only make this post longer than it already is. So, I will refer you to Leonid Libkin's Elements of Finite Model Theory for more on this (and also for the proper acknowledgement of these results!).