Finite model theory studies logical definability and equivalence on finite first-order structures. Unlike unrestricted model theory, first-order compactness is unavailable when models are required to be finite. Locality, bounded-variable games and descriptive characterizations of complexity classes are central tools.
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- neighbourhood is the induced structure on the union of its radius- graph balls, with the tuple marked by constants.
For a finite relational signature and quantifier rank , matching the numbers of all marked radius- one-point neighbourhood types suffices for two finite structures to satisfy the same first-order sentences of rank at most . 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.
Articles by others on the same topic
Finite model theory is a branch of mathematical logic that focuses on the study of finite structures and the properties of sentences in various logical languages when interpreted over these structures. It examines models that have a finite domain, meaning the set of elements that satisfy the sentences of the theory is finite.