Finite model theory is a subarea of model theory. Model theory is the branch of logic which deals with the relation between a formal language (syntax) and its interpretations (semantics). Finite model theory is a restriction of model theory to interpretations on finite structures, which have a finite universe.
Since many central theorems of model theory do not hold when restricted to finite structures, finite model theory is quite different from model theory in its methods of proof. Central results of classical model theory that fail for finite structures under finite model theory include the compactness theorem, Gödel's completeness theorem, and the method of ultraproducts for first-order logic (FO). While model theory has many applications to mathematical algebra, finite model theory became an "unusually effective" instrument in computer science. In other words: "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." Thus the main application areas of finite model theory are: descriptive complexity theory, database theory and formal language theory.
Axiomatisability
A common motivating question in finite model theory is whether a given class of structures can be described in a given language. For instance, one might ask whether the class of cyclic graphs can be distinguished among graphs by a FO sentence, which can also be phrased as asking whether cyclicity is FO-expressible.
A single finite structure can always be axiomatized in first-order logic, where axiomatized in a language L means described uniquely up to isomorphism by a single L-sentence. Similarly, any finite collection of finite structures can always be axiomatized in first-order logic. Some, but not all, infinite collections of finite structures can also be axiomatized by a single first-order sentence.
Characterisation of a single structure
Is a language L expressive enough to axiomatize a single finite structure S?
Problem
A structure like (1) in the figure can be described by FO sentences in the logic of graphs like
Every node has an edge to another node: No node has an edge to itself: There is at least one node that is connected to all others:
However, these properties do not axiomatize the structure, since for structure (1') the above properties hold as well, yet structures (1) and (1') are not isomorphic.
Informally the question is whether by adding enough properties, these properties together describe exactly (1) and are valid (all together) for no other structure (up to isomorphism).
Approach
For a single finite structure it is always possible to precisely describe the structure by a single FO sentence. The principle is illustrated here for a structure with one binary relation and without constants: say that there are at least elements: say that there are at most elements: state every element of the relation : state every non-element of the relation :
all for the same tuple , yielding the FO sentence .
Extension to a fixed number of structures
The method of describing a single structure by means of a first-order sentence can easily be extended for any fixed number of structures. A unique description can be obtained by the disjunction of the descriptions for each structure. For instance, for two structures and with defining sentences and this would be
Extension to an infinite structure
By definition, a set containing an infinite structure falls outside the area that FMT deals with. Note that infinite structures can never be discriminated in FO, because of the Löwenheim–Skolem theorem, which implies that no first-order theory with an infinite model can have a unique model up to isomorphism.
The most famous example is probably Skolem's theorem, that there is a countable non-standard model of arithmetic.
Characterisation of a class of structures
Is a language L expressive enough to describe exactly (up to isomorphism) those finite structures that have certain property P?
Problem
The descriptions given so far all specify the number of elements of the universe. Unfortunately most interesting sets of structures are not restricted to a certain size, like all graphs that are trees, are connected or are acyclic. Thus to discriminate a finite number of structures is of special importance.
Approach
Instead of a general statement, the following is a sketch of a methodology to differentiate between structures that can and cannot be discriminated.