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. In mathematics, model theory is the study of the representation of mathematical concepts in terms of set theory, or the study of the models which underlie mathematical systems. ... First-order predicate calculus or first-order logic (FOL) permits the formulation of quantified statements such as there exists an x such that. ... In mathematics, a finite group is a group which has finitely many elements. ... A database is a collection of information stored in a computer in a systematic way, such that a computer program can consult it to answer questions. ... An abstract machine, also called an abstract computer, is a theoretical model of a computer hardware or software system. ... Discrete mathematics, sometimes called finite mathematics, is the study of mathematical structures that are fundamentally discrete, in the sense of not supporting or requiring the notion of continuity. ... Complexity theory can refer to more than one thing: Computational complexity theory: a field in theoretical computer science and mathematics dealing with the resources required during computation to solve a given problem Systems theory (or systemics or general systems theory): an interdisciplinary field including engineering, biology and philosophy that incorporates... A database is an information set with a regular structure. ...

Many important results of first-order logic and classical model theory fail when restricted to finite structures, including the compactness theorem, the Crag interpolation theorem, 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. The compactness theorem is a basic fact in symbolic logic and model theory and asserts that a set (possibly infinite) of first-order sentences is satisfiable, i. ... In mathematical logic, the classic Löwenheim- Skolem theorem states that any infinite model M has a countably infinite submodel N that satisfies exactly the same set of first-order sentences that M satisfies. ... Gödels completeness theorem is a fundamental theorem in mathematical logic proved by Kurt Gödel in 1929. ... In mathematics, the transitive closure of a binary relation R on a set X is the smallest transitive relation on X that contains R. For any relation R the transitive closure of R always exists. ... In mathematics, the least fixed point in order theory of a function is the fixed point which is less than or equal to all other fixed points, according to some partial order. ...

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." Descriptive complexity is a branch of finite model theory, a subfield of computational complexity theory and mathematical logic, in which we seek to characterize complexity classes by the type of logic needed to express the languages in them. ... The Turing machine is an abstract machine introduced in 1936 by Alan Turing to give a mathematically precise definition of algorithm or mechanical procedure. As such it is still widely used in theoretical computer science, especially in complexity theory and the theory of computation. ... In computational complexity theory, P is the complexity class containing decision problems which can be solved by a deterministic Turing machine using a polynomial amount of computation time, or polynomial time. ...

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. In mathematics and computer science, graph theory studies the properties of graphs. ... A randomized algorithm is an algorithm which is allowed to flip a truly random coin. ...

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

External links

• Jouko Väänänen. A Short Course on Finite Model Theory (http://www.math.helsinki.fi/logic/people/jouko.vaananen/shortcourse.pdf). Department of Mathematics, University of Helsinki. Based on lectures from 1993-1994.
• Finite Model Theory Homepage (http://www-mgi.informatik.rwth-aachen.de/FMT/) at Aachen Universitory of Technology, including a list of open problems
• Finite Model Theory References (http://www.ldc.usb.ve/~arratia/refs/ref.html), a database of references related to finite model theory