No compactness in finite model theory

The compactness theorem for first-order logic is indisputably the most fundamental theorem in model theory. It says that

A theory has a model iff every finite subset of it has a model

I will say no more about the usefulness of this theorem in model theory. But what I will speak about now is the failure of compactness in finite model theory, as I already remarked before.

In finite model theory (FMT), we are only concerned with finite structures. Hence compactness theorem in FMT would read

A theory has a finite model iff every subset of it has a finite model


It is easy to conjure a counterexample for this statement. Consider the first-order theory `T` over the empty vocabulary containing sentences of the following form (for all `k >= 2`):

`S_k = EE x_1,...,x_k( x_1 != x_2 ^^ x_1 != x_3 ^^ cdots ^^ x_{k-1} != x_k )`

It is easy to see that every subset `T'` of `T` has a finite model; if `n` is the largest integer such that `S_n in T'`, then the structure containing `n` elements satisfies `T'`. It is also easy to see that `T` has no finite model. (QED)

Likewise, many other fundamental theorems in model theory, such as Craig Interpolation Theorem, are also casualties of finitization (more on this later); Ehrenfeucht-Fraisse games being the only general tool available for proving inexpressibility results in finite model theory.