Finite model theory is a subarea ofmodel theory. Model theory is the branch oflogic which deals with the relation between a formal language (syntax) and its interpretations (semantics). Finite model theory is a restriction of model theory tointerpretations on finitestructures, 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 thecompactness theorem,Gödel's completeness theorem, and the method ofultraproducts forfirst-order logic (FO). These invalidities all follow fromTrakhtenbrot's theorem.^[1]

While model theory has many applications tomathematical algebra, finite model theory became an "unusually effective"^[2] 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."^[3] Thus the main application areas of finite model theory are:descriptive complexity theory,database theory andformal language theory.

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 languageL means described uniquely up to isomorphism by a singleL-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.

Is a languageL expressive enough to axiomatize a single finite structureS?

A structure like (1) in the figure can be described by FO sentences in thelogic of graphs like

1. Every node has an edge to another node:${\displaystyle {\mathrm{\forall }}_x{\mathrm{\exists }}_{y}G(x,y).}$
2. No node has an edge to itself:${\displaystyle {\mathrm{\forall }}_{x,y}(G(x,y)\Rightarrow x\ne y).}$
3. There is at least onenode that is connected to all others:${\displaystyle {\mathrm{\exists }}_x{\mathrm{\forall }}_y(x\ne y\Rightarrow G(x,y)).}$

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).

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${\displaystyle R}$ and without constants:

1. say that there are at least${\displaystyle n}$ elements:${\displaystyle {\phi }_1=\underset{i\ne j}{\bigwedge }\mathrm{\neg }(x_i=x_j)}$
2. say that there are at most${\displaystyle n}$ elements:${\displaystyle {\phi }_2={\mathrm{\forall }}_y\underset{i}{\bigvee }(x_i=y)}$
3. state every element of the relation${\displaystyle R}$:${\displaystyle {\phi }_3=\underset{(a_i,a_j)\in R}{\bigwedge }R(x_i,x_j)}$
4. state every non-element of the relation${\displaystyle R}$:${\displaystyle {\phi }_4=\underset{(a_i,a_j)\notin R}{\bigwedge }\mathrm{\neg }R(x_i,x_j)}$

all for the same tuple${\displaystyle x_1..x_n}$, yielding the FO sentence${\displaystyle {\mathrm{\exists }}_{x_1}\dots {\mathrm{\exists }}_{x_n}({\phi }_1\wedge {\phi }_2\wedge {\phi }_3\wedge {\phi }_4)}$.

The method of describing a single finite 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 finite structures${\displaystyle A}$ and${\displaystyle B}$ with defining sentences${\displaystyle {\phi }_A}$ and${\displaystyle {\phi }_B}$ this would be

${\displaystyle {\phi }_A\vee {\phi }_B.}$

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 theLö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 probablySkolem's theorem, that there is a countable non-standard model of arithmetic.

Is a languageL expressive enough to describe exactly (up to isomorphism) those finite structures that have certain propertyP?

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.

Instead of a general statement, the following is a sketch of a methodology to differentiate between structures that can and cannot be discriminated.

We want to show that the property that the size of an ordered structureA = (A, ≤) is even, can not be expressed in FO.

1. The idea is to pickA ∈ EVEN andB ∉ EVEN, where EVEN is the class of all structures of even size.
2. We start with two ordered structuresA₂ andB₂ with universes A₂ = {1, 2, 3, 4} and B₂ = {1, 2, 3}. ObviouslyA₂ ∈ EVEN andB₂ ∉ EVEN.
3. Form = 2, we can now show* that in a 2-moveEhrenfeucht–Fraïssé game onA₂ andB₂ the duplicator always wins, and thusA₂ andB₂ cannot be discriminated in FO[2], i.e.${\displaystyle {\mathbf{A}}_2\models \alpha ⟺{\mathbf{B}}_2\models \alpha }$ for everyα ∈ FO[2].
4. Next we have to scale the structures up by increasingm. For example, form = 3 we must find anA₃ andB₃ such that the duplicator always wins the 3-move game. This can be achieved by A₃ = {1, ..., 8} and B₃ = {1, ..., 7}. More generally, we can choose A_m = {1, ..., 2^m} and B_m = {1, ..., 2^m−1}; for anym the duplicator always wins them-move game for this pair of structures*.
5. Thus EVEN on finite ordered structures cannot be expressed in FO.

(*) Note that the proof of the result of theEhrenfeucht–Fraïssé game has been omitted, since it is not the main focus here.

Glebskiĭ et al. (1969) and, independently,Fagin (1976) proved a zero–one law for first-order sentences in finite models; Fagin's proof used thecompactness theorem. According to this result, every first-order sentence in a relational signature${\displaystyle \sigma }$ is eitheralmost always true or almost always false in finite${\displaystyle \sigma }$-structures. That is, letS be a fixed first-order sentence, and choose a random${\displaystyle \sigma }$-structure${\displaystyle G_n}$ with domain${\displaystyle \{1,\dots ,n\}}$, uniformly among all${\displaystyle \sigma }$-structures with domain${\displaystyle \{1,\dots ,n\}}$. Then in the limit asn tends to infinity, the probability thatG_n modelsS will tend either to zero or to one:

${\displaystyle \underset{n\to \mathrm{\infty }}{lim}\mathrm{Pr}[G_n\models S]\in \{0,1\}.}$

The problem of determining whether a given sentence has probability tending to zero or to one isPSPACE-complete.^[4]

A similar analysis has been performed for more expressive logics than first-order logic. The 0-1 law has been shown to hold for sentences inFO(LFP), first-order logic augmented with a least fixed point operator, and more generally for sentences in the infinitary logic${\displaystyle L_{\mathrm{\infty }\omega }^{\omega }}$, which allows for potentially arbitrarily long conjunctions and disjunctions.Another important variant is the unlabelled 0-1 law, where instead of considering the fraction of structures with domain${\displaystyle \{1,\dots ,n\}}$, one considers the fraction of isomorphism classes of structures withn elements. This fraction is well-defined, since any two isomorphic structures satisfy the same sentences. The unlabelled 0-1 law also holds for${\displaystyle L_{\mathrm{\infty }\omega }^{\omega }}$ and therefore in particular for FO(LFP) and first-order logic.^[5]

An important goal of finite model theory is the characterisation ofcomplexity classes by the type oflogic needed to express the languages in them. For example,PH, the union of all complexity classes in the polynomial hierarchy, is precisely the class of languages expressible by statements ofsecond-order logic. This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods and providing additional evidence that the main complexity classes are somehow "natural" and not tied to the specificabstract machines used to define them.

Specifically, eachlogical system produces a set ofqueries expressible in it. The queries – when restricted to finite structures – correspond to thecomputational problems of traditional complexity theory.

Some well-known complexity classes are captured by logical languages as follows:

• In the presence of a linear order, first-order logic with a commutative,transitive closure operator added yieldsL, problems solvable in logarithmic space.
• In the presence of a linear order, first-order logic with atransitive closure operator yieldsNL, the problems solvable in nondeterministic logarithmic space.
• In the presence of a linear order, first-order logic with aleast fixed point operator givesP, the problems solvable in deterministic polynomial time.
• On all finite structures (regardless of whether they are ordered),Existential second-order logic givesNP (Fagin's theorem).^[6]

A substantial fragment ofSQL (namely that which is effectivelyrelational algebra) is based on first-order logic (more precisely can be translated indomain relational calculus by means ofCodd's theorem), as the following example illustrates: Think of a database table "GIRLS" with the columns "FIRST_NAME" and "LAST_NAME". This corresponds to a binary relation, say G(f, l) on FIRST_NAME × LAST_NAME. The FO query${\displaystyle l:G(\text{'Judy'},l)}$, which returns all the last names where the first name is 'Judy', would look in SQL like this:

selectLAST_NAMEfromGIRLSwhereFIRST_NAME='Judy'

Notice, we assume here, that all last names appear only once (or we should use SELECT DISTINCT since we assume that relations and answers are sets, not bags).

Next we want to make a more complex statement. Therefore, in addition to the "GIRLS" table we have a table "BOYS" also with the columns "FIRST_NAME" and "LAST_NAME". Now we want to query the names of all the girls that have the same last name as at least one of the boys. The FO query is${\displaystyle (f,l):\mathrm{\exists }h(G(f,l)\wedge B(h,l))}$, and the corresponding SQL statement is:

selectFIRST_NAME,LAST_NAMEfromGIRLSwhereLAST_NAMEIN(selectLAST_NAMEfromBOYS);

Notice that in order to express the "∧" we introduced the new language element "IN" with a subsequent select statement. This makes the language more expressive for the price of higher difficulty to learn and implement. This is a common trade-off in formal language design. The way shown above ("IN") is by far not the only one to extend the language. An alternative way is e.g. to introduce a "JOIN" operator, that is:

selectdistinctg.FIRST_NAME,g.LAST_NAMEfromGIRLSg,BOYSbwhereg.LAST_NAME=b.LAST_NAME;

First-order logic is too restrictive for some database applications, for instance because of its inability to expresstransitive closure. This has led to more powerful constructs being added to database query languages, such asrecursive WITH inSQL:1999. More expressive logics, likefixpoint logics, have therefore been studied in finite model theory because of their relevance to database theory and applications.

Narrative data contains no defined relations. Thus the logical structure of text search queries can be expressed inpropositional logic, like in:

("Java" AND NOT "island") OR ("C#" AND NOT "music")

Note that the challenges in full text search are different from database querying, like ranking of results.

• Trakhtenbrot 1950: failure of completeness theorem in first-order logic
• Scholz 1952: characterisation ofspectra in first-order logic
• Fagin 1974: the set of all properties expressible in existential second-order logic is precisely the complexity class NP
• Chandra, Harel 1979/80: fixed-point first-order logic extension for database query languages capable of expressing transitive closure -> queries as central objects of FMT
• Immerman,Vardi 1982: fixed-point logic over ordered structures captures PTIME -> descriptive complexity (Immerman–Szelepcsényi theorem)
• Ebbinghaus, Flum 1995: first comprehensive book "Finite Model Theory"
• Abiteboul, Hull,Vianu 1995: book "Foundations of Databases"
• Immerman 1999: book "Descriptive Complexity"
• Kuper, Libkin, Paredaens 2000: book "Constraint Databases"
• Darmstadt 2005/ Aachen 2006: first international workshops on "Algorithmic Model Theory"

• Ebbinghaus, Heinz-Dieter; Flum, Jörg (1995).Finite Model Theory.Springer.ISBN 978-3-540-60149-4.

• Fagin, Ronald (1976). "Probabilities on Finite Models".The Journal of Symbolic Logic.41 (1):50–58.doi:10.2307/2272945.JSTOR 2272945.
• Glebskiĭ, Yu V.; Kogan, D. I.; Liogon'kiĭ, M. I.; Talanov, V. A. (1969). "Объем и доля выполнимости формул узкого исчисления предикатов" [Volume and fraction of satisfiability of formulae of the first-order predicate calculus].Kibernetika.5 (2):17–27. Also available as;"Range and degree of realizability of formulas in the restricted predicate calculus".Cybernetics.5 (2):142–154. 1972.doi:10.1007/BF01071084.
• Libkin, Leonid (2004).Elements of Finite Model Theory.Springer.ISBN 3-540-21202-7.

• Abiteboul, Serge; Hull, Richard; Vianu, Victor (1995).Foundations of Databases.Addison-Wesley.ISBN 0-201-53771-0.

• Immerman, Neil (1999).Descriptive Complexity. New York:Springer.ISBN 0-387-98600-6.

• Grädel, Erich; Kolaitis, Phokion G.;Libkin, Leonid; Maarten, Marx;Spencer, Joel;Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007).Finite model theory and its applications. Texts in Theoretical Computer Science. An EATCS Series. Berlin:Springer-Verlag.ISBN 978-3-540-00428-8.Zbl 1133.03001.

Wikibooks has a book on the topic of:Finite Model Theory

• Libkin, Leonid (2009). "The finite model theory toolbox of a database theoretician".PODS 2009: Proceedings of the twenty-eighth ACM SIGACT–SIGMOD symposium on Principles of database systems. pp. 65–76.doi:10.1145/1559795.1559807. Also suitable as a general introduction and overview.
• Leonid Libkin.Introductory chapter of "Elements of Finite Model Theory"Archived 2015-09-24 at theWayback Machine. Motivates three main application areas: databases, complexity and formal languages.
• Jouko Väänänen.A Short Course on Finite Model Theory. Department of Mathematics, University of Helsinki. Based on lectures from 1993 to 1994.
• Anuj Dawar.Infinite and Finite Model Theory, slides, University of Cambridge, 2002.
• "Algorithmic Model Theory". RWTH Aachen. Archived fromthe original on 17 July 2012. Retrieved7 November 2013. Includes a list of open FMT problems.

• Finite model theory
• Model theory

• Articles with short description
• Short description matches Wikidata
• Webarchive template wayback links
• Pages that use a deprecated format of the math tags