Finite model theory

From Wikipedia, the free encyclopedia

Finite model theory is a subfield of model theory that focuses on properties of logical languages, such as first-order logic, over finite structures, such as finite groups, graphs, databases, and most abstract machines. It focuses in particular on connections between logical languages and computation, and is closely associated with discrete mathematics, complexity theory, and database theory.

Many important results of first-order logic and classical model theory fail when restricted to finite structures, including the compactness theorem, the Craig interpolation lemma, the Los-Tarski preservation theorem, the Downward Löwenheim-Skolem theorem, and Gödel's completeness theorem. The essential problem is that in this context, first-order logic is not sufficiently expressive. By extending first-order logic with operators such as transitive closure and least fixed point, and by using fragments of second-order logic, we obtain new logics that have more interesting properties over finite structures.

One important subfield of finite model theory, descriptive complexity, connects the expressivity of various logical languages with the capabilities of various abstract machines. For example, if a language can be expressed in first-order logic with a least fixed point operator added, a Turing machine can determine in polynomial time (see P) whether a given string is in the language. Descriptive complexity allows results to be transferred between computational complexity and mathematical logic and gives additional evidence that the standard complexity classes are "natural." Neil Immerman states "In the history of mathematical logic most interest has concentrated on infinite structures....Yet, the objects computers have and hold are always finite. To study computation we need a theory of finite structures."^[1]

Another important result of finite model theory are the zero-one laws, which establish that many types of logical formulas hold for either almost all or almost no finite structures. For example, the proportion of graphs of size n that are connected approaches one as n approaches infinity, while the proportion that contain an isolated vertex approaches zero. In fact the same is true of any graph property that can be checked in polynomial time: it either approaches one or approaches zero. This has ramifications for randomized algorithms on large finite structures.

Finite model theory also studies finite restrictions of logic, such as first-order logic with only a fixed limit of k variables.