*complete*, criterion for determining expressibility (ie, definability) of a query in a logic (such as, first-order logic) on finite structures. For example, we may ask if the query

*connectivity*for finite graphs, which asks whether a finite graph is connected, is expressible in first-order logic. The answer is 'no', though we won't prove this now. [Curious readers are referred to Libkin's Elements of Finite Model Theory or Fagin's excellent survey paper.]

We shall start by recalling the notion of homomorphisms and isomorphisms between structures. Given two `sigma`-structures `fr A` and `fr B`, a

*homomorphism*between them is a function `h: A -> B` such that `h(c^{fr A}) = c^{fr B}` for every constant symbol `c in sigma`, and `h(bb a) := (h(a_1), ..., h(a_r)) in R^{fr B}`, for every `r`-ary relation symbol `R in sigma` and `bb a := (a_1,...,a_r) in R^{fr A}`. So, homomorphisms are

*tuple-preserving*functions (here, think of a tuple as an `r`-ary vector prepended by an `r`-ary relation symbol, eg, `R(1,2,3)`). Now

*isomorphisms*are basically bijective homomorphisms whose inverse are also homomorphisms. Intuitively, this means that two isomorphic structures are the same after

*relabeling the elements of the universe in one of these structures*. We write `fr A ~= fr B` to denote that `fr A` and `fr B` be isomorphic.

Now we define what we mean by

*queries*. Fix a vocabulary `sigma` and a class `cc M` of (not necessarily all) finite `sigma`-structures. This class `cc M` will be referred to as a

*ground set*. Now, for `k >= 0`, a `k`-ary query `cc Q` is a function associating each `fr A in cc M` to a subset of `A^k` such that `cc Q` is closed under isomorphisms, ie, whenever `h: A -> B` is an isomorphism, we have `h( cc Q(fr A)) = cc Q(fr B)`. Now this query `cc Q` is said to be

*expressible*(or

*definable*) in a logic `L` over `cc M` if there exists a `L`-formula `phi` over `sigma` with `k` free variables such that for every `fr A in cc M`, `cc Q(fr A) = phi(fr A)` where

`phi(fr A) := { (a_1,...,a_k) in A^k : fr A |= phi(a_1,...,a_k) }`.

Whenever `cc M` be the set of

*all*finite structures, we shall omit mention of `cc M`.

An important special case occurs when `k = 0`. Such queries are normally called

*boolean queries*or just

*properties*. In this case, the image of `cc Q` can only be either a singleton `{()}` containing the trivial tuple `()`, or the empty set `O/`. We will identify `{()}` with `true` and `O/` with `false`. So, a property `cc Q` is expressible in a logic `L` over `cc M` if there exists an `L`-sentence `phi` over `sigma` such that `cc Q(fr A) = true` iff `fr A |= phi`, for each `fr A in cc M`. Examples of boolean queries (for finite graphs) are:

- Hamiltonian: `cc Q(fr G) = true` iff the graph `fr G` is hamiltonian.

- Self-loop: `cc Q(fr G) = true` iff the graph `fr G` has a self-loop (ie, `fr G |= EE x( E(x,x))`).

- Isolated: `cc Q(fr G) = true` iff the graph `fr G` has an isolated vertex.

- Connected: `cc Q(fr G) = true` iff the graph `fr G` is connected.

- Acyclic: `cc Q(fr G) = true` iff the graph `fr G` is acyclic.

An example of 2-ary queries is the transitive closure query of finite graphs:

`Q: fr G |-> { (a,b) in G^2 : text{there exists a path from } a text{ to } b text{ in} fr G }`

Question: which of the above queries are expressible in first-order logic? Well, we already saw that

*Self-loop*is expressible in first-order logic. So, it is enough to exhibit a first-order formula to show that a query be expressible in first-order logic. But how do we prove first-order inexpressibility results? In classical model theory, we have tools like compactness and Lowenheim-Skolem theorems for proving first-order inexpressibility. However, most of these tools including the two afore-mentioned theorems fail to "work" in the finite. The only one result that survives is the Ehrenfeucht-Fraisse games (a good exposition of the result can be found here). [Incidentally, does this imply that finite model theory is more difficult than classical model theory?] The games, for example, can be used to prove that the queries Hamiltonian, Connected, Acyclic, and Transitive Closure are not definable in first-order logic. These results will be discussed in subsequent postings.

## No comments:

Post a Comment