Finite model theory

Finite model theory studies first-order structures restricted to finite domains, and asks which properties can be expressed in specified formal languages. The restriction changes the available tools: ordinary first-order compactness does not hold when only finite models are admitted.

For example, the sentences saying there are at least $n$ distinct elements, one for every positive integer $n$, have a finite model for each finite subset but no common finite model. This is a direct failure of finite compactness. Logical games, locality, and bounded-variable fragments then compare the expressive power of formulas on finite databases and graphs, linking definability with computational complexity theory.

Two formulas with the same free variables are asymptotically equivalent when the probability of their universal equivalence tends to one over the chosen finite-structure distribution. If a quantifier-eliminating extension theory has all its axioms of asymptotic probability one, compactness makes every formula asymptotically equivalent to a quantifier-free one: each particular equivalence follows from finitely many axioms, whose conjunction still has limiting probability one.

Extend first-order logic by iterating definable relation operators from the empty relation. If iteration reaches a fixed point, use that relation; if it enters a nontrivial cycle, the partial fixed point is the empty relation. For a fixed arity on a finite universe, a relation requires polynomially many bits and there are exponentially many states, so iteration is evaluable in PSPACE. On finite ordered structures this logic captures PSPACE.

For a relational structure, the Gaifman graph has the same universe. Two distinct elements are adjacent if they occur together in some tuple of some interpreted relation. A tuple's radius-$r$ neighbourhood is the induced structure on the union of its radius-$r$ graph balls, with the tuple marked by constants.

For a finite relational signature and quantifier rank $q$, matching the numbers of all marked radius-$3^q$ one-point neighbourhood types suffices for two finite structures to satisfy the same first-order sentences of rank at most $q$. Equivalently, a bijection can match the isomorphism types of these marked neighbourhoods point by point. On bounded-degree structures, a threshold version permits large neighbourhood-type counts to differ once both exceed a fixed bound. Long cycles of equal total size give useful exact-count applications.