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 if a given string is in the language in polynomial time (see P). Descriptive complexity allows results to be transferred between computational complexity and mathematical logic and gives additional evidence that the standard complexity classes are "natural."

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.

• R. Fagin. Finite model theory-a personal perspective. Theoretical Computer Science 116, 1993, pp. 3-31.
• Jouko Väänänen. A Short Course on Finite Model Theory. Department of Mathematics, University of Helsinki. Based on lectures from 1993-1994.
• Finite Model Theory Homepage at Aachen University of Technology, including a list of open problems
• Finite Model Theory References, a database of references related to finite model theory
• Introductory chapter on Finite Model Theory in Wikibook Logic for Computer Scientists