Finite Model Theory: Preliminaries (1)

I realize that in the previous postings I haven't been as precise as I can possibly be. It's all about to change: we shall now fix terminologies for our subsequent discussion on finite model theory. We will however have to divide this "section" into two postings, as it is too long for one. We shall also assume that the reader knows basic facts from mathematical logic (see Enderton's A Mathematical Introduction To Logic).

We can start by discussing what finite model theory is. One common definition for finite model theory is the model theory of finite structures. Precise, but perhaps too succinct. What makes it different from classical model theory? Finite model theory is primarily concerned with finite structures, while model theory with both finite and infinite structures. Hence, one can expect that the definitions used in finite model theory are very similar to those in classical model theory. The restriction to finite structures is necessary for studying computers and computation due to their finite nature. Note also that finiteness doesn't necessarily imply triviality. For example, witness that (finite) graph theory is a deep, rich, and beautiful subject, which has captivated brilliant mathematicians from many generations including Euler and Erdos.

Unless otherwise stated, we shall make the following assumptions in subsequent postings on finite model theory:

• Every vocabulary and structure is relational, ie, has no function symbols and functions.
  
• Every vocabulary has finitely many (constant and relation) symbols.
  
• Capital Fraktur fonts are used to denote structures; their corresponding letters in Latin correspond to their universes. For example, a structure `fr A` has universe `A`.
  

I am going to adopt an extremely useful definition of expansion of structures from Libkin's Elements of Finite Model Theory, which will allow us to convert back and forth between formulas and sentences. Let `fr A` and `fr A'` be structures over, respectively, `sigma` and `sigma'` where `sigma nn sigma' = O/`. The expansion of `fr A` by `fr A'`, denoted by `(fr A,fr A')`, is the `sigma uu sigma'`-structure with all symbols from `sigma` interpreted according to `fr A`, and from `sigma'` interpreted according to `fr A'`. An important special case is when `sigma'` be the vocabulary `sigma_n` containing only constant symbols `c_1,cdots,c_n`. In this case, if `fr A' = (a_1, cdots, a_n)` (with `a_i` interpreting `c_i`), we can omit some redundant brackets and write `(fr A, fr A') = (fr A, a_1, cdots, a_n)`. We have the following lemma:

Lemma: Suppose `phi(x_1, cdots, x_n)` be a `sigma`-formula, and `fr A` be a `sigma`-structure. Let `Phi` be the formula `phi(c_1/x_1,cdots,c_n/x_n)`, ie, each occurence of `x_i` is replaced by a brand new constant symbol `c_i`. Then, we have: `fr A |= phi(a_1,cdots,a_n)` iff `(fr A,a_1,cdots,a_n) |= Phi`.

Finally, we need to define the notion of `k`-ary queries, which we will do in the next posting.