Finite model theory
Encyclopedia
Finite Model Theory is a subarea of model theory
(MT). MT is the branch of mathematical logic
which deals with the relation between a formal language (syntax) and its interpretations (semantics). FMT is a restriction of MT to interpretations
of finite structures
, i.e. structures with a finite universe.
Proofs:Since many central theorems of MT do not hold when restricted to finite structures, FMT is quite different from MT in proof methods. Failing central results include the compactness theorem
, Gödel's completeness theorem
, and the method of ultraproduct
s for first-order logic. Some concepts become meaningless like that of types (and thus need to be redefined in FMT). Other methods like Ehrenfeucht games become more central in FMT.
Finiteness: As MT is closely related to mathematical algebra, FMT became an "unusually effective" instrument in computer science. This may have its origin in the fact that the valid first order (henceforth FO) sentences over all finite structures are not recursively enumerable, i.e. from a mathematical point of view they are 'just' finite but computer scientifically they can be seen as quite complex objects of study. 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."
Applications: The area of descriptive complexity theory
connects complexity classes with structures and sentences of logics, to gain new insights and justifications to computational complexity. In database theory
query languages can be formalized by parts and extensions of FO. In formal language theory
the expressive power of languages corresponds to certain logics on finite structures.
Character: FMT is mainly about discrimination of structures: Every single finite structure can be characterized in a single FO sentence up to isomorphy. This doesn't hold for classes of finite structures. Thus methods are required to determine if a class of structures can be discriminated in a certain language, e.g. games, locality, 0-1 laws, also extensions of FO can be thought of in order to discriminate these classes, fixed point logics,or sub-SO logics, as well as assumptions can be made on the structure, e.g. that it's ordered or is a string. Finite model theory also studies finite restrictions of logic, such as first-order logic with only a fixed limit of k variables as well as hybrid structures, where nonfinite structures are embedded in finite ones.
Now do these properties describe the structure uniquely (up to isomorphism)? Obviously not since for structure (1') the above properties hold as well.
Simply put, the question is, if one adds enough properties, is it possible that these properties (all together) describe exactly (1) and are valid (all together) for no other structure (up to isomorphy).
all for the same tuple
, i.e. 
.
Writing down a sequence of, say 67, descriptions is easy in theory, but quite impractical. This is a well known problem from programming, where one would use a for loop from 1 to 67 instead. This isn't dealt with in depth here, but mentioned to show that there are more issues to a language than just its expressiveness.
1. The core idea is that whenever one wants to see if a Property P can be expressed in FO, one chooses Structures A and B, where A does have P and B doesn't. If for A and B the same FO sentences hold P cannot be expressed in FO (else it can). For short:
A ∈ P, B ∉ P and A ≡ B
where A ≡ B is A |= α ⇔ B |= α for all FO-sentences α, and P is the class of Structures with property P.
2. The actual methodology partitions the language, like FO, into countably many classes FO[m], such that for each m the above (core idea) has to be shown. That is:
A ∈ P, B ∉ P and A ≡m B
with a pair A, B for each m and α (in ≡) from FO[m].
3. A partition FO[m] can be obtained by the quantifier rank qr(α) of a FO formula α. It expresses the depth of quantifier nesting. For example for a formula in prenex normal form
qr gives simply the total number of its quantifiers. So FO[m] is defined as all FO formulas α with qr(α) ≤ m.
4. Thus it all comes down to show A |= α ⇔ B |= α on the partitions FO[m]. The main approach here is to use the algebraic characterization provided by Ehrenfeucht-Fraisse Games. What they do is roughly, take a single partial isomorphism on A and B and extend it m times, in order to either prove or disprove A ≡m B, dependent on who wins the game.
1. Therefore we start with 2 ordered structures A2 and B with universes A2 = {1, 2, 3, 4} and B2 = {1, 2, 3, 4, 5}. Obviously A2 ∈ EVEN and B2 ∉ EVEN, where EVEN is the class of all structures of even size. Now we can show that in a 2-move Ehrenfeucht Fraisse Game (i.e. m = 2, what explains the subscrpts above) on A2 and B2 the duplicator always wins, and thus A2 and B2 cannot be discriminated in FO[2], i.e. A2 |= FO[2] ⇔ B2 |= FO[2].
2. Next we have to scale the structures up by increasing m. For m = 3 we must find an A3 and B3 s.t. the duplicator wins the game. This can be achieved by A3 = {1, ..., 8} and B3 = {1, ..., 9}.
3. More general we choose Am = {1, ..., 2m} and Bm = {1, ..., 2m+1} where we can prove that the duplicator always wins. Thus EVEN on finite ordered structures cannot be expressed in FO qed.
The most famous example is probably Skolem's theorem: there is a countable non-standard model of arithmetic.
SELECT *
FROM posting
WHERE posting.answers = '1234';
To obtain the children and grandchildren of "1234" we write:
SELECT * FROM posting
WHERE posting.answers = '1234' OR posting.answers =
(
SELECT id FROM posting
WHERE posting.answers = '1234';
)
For a fixed number of generations this can be extended in SQL (although writing a query for 67 generations is not really a nice job). However we don't know how long a single thread can get. All we know is it must be of finite length. This cannot be expressed in the SQL expressions used above. Therefore we need an extension such as "START WITH ... CONNECT BY ...":
SELECT * FROM posting
START WITH posting.id = '1234'
CONNECT BY PRIOR posting.id = posting.answers;
All the above correspond to logic expressions. The 1st and 2nd query can be expressed in FO, whereas the 3rd query requires some extension like fixed-point-logics.
answers( x, 1234 )
answers( x, 1234 ) ∨ ∃y ( answers( x, y ) ∧ answers( y, 1234 ) )
...
Model theory
In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
(MT). MT is the branch of mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
which deals with the relation between a formal language (syntax) and its interpretations (semantics). FMT is a restriction of MT to interpretations
Interpretation (logic)
An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...
of finite structures
Structure (mathematical logic)
In universal algebra and in model theory, a structure consists of a set along with a collection of finitary operations and relations which are defined on it....
, i.e. structures with a finite universe.
Proofs:Since many central theorems of MT do not hold when restricted to finite structures, FMT is quite different from MT in proof methods. Failing central results include the compactness theorem
Compactness theorem
In mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model...
, Gödel's completeness theorem
Gödel's completeness theorem
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....
, and the method of ultraproduct
Ultraproduct
The ultraproduct is a mathematical construction that appears mainly in abstract algebra and in model theory, a branch of mathematical logic. An ultraproduct is a quotient of the direct product of a family of structures. All factors need to have the same signature...
s for first-order logic. Some concepts become meaningless like that of types (and thus need to be redefined in FMT). Other methods like Ehrenfeucht games become more central in FMT.
Finiteness: As MT is closely related to mathematical algebra, FMT became an "unusually effective" instrument in computer science. This may have its origin in the fact that the valid first order (henceforth FO) sentences over all finite structures are not recursively enumerable, i.e. from a mathematical point of view they are 'just' finite but computer scientifically they can be seen as quite complex objects of study. 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."
Applications: The area of descriptive complexity theory
Descriptive complexity
Descriptive complexity is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity classes in the polynomial hierarchy, is precisely the...
connects complexity classes with structures and sentences of logics, to gain new insights and justifications to computational complexity. In database theory
Database theory
Database theory encapsulates a broad range of topics related to the study and research of the theoretical realm of databases and database management systems....
query languages can be formalized by parts and extensions of FO. In formal language theory
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
the expressive power of languages corresponds to certain logics on finite structures.
Character: FMT is mainly about discrimination of structures: Every single finite structure can be characterized in a single FO sentence up to isomorphy. This doesn't hold for classes of finite structures. Thus methods are required to determine if a class of structures can be discriminated in a certain language, e.g. games, locality, 0-1 laws, also extensions of FO can be thought of in order to discriminate these classes, fixed point logics,or sub-SO logics, as well as assumptions can be made on the structure, e.g. that it's ordered or is a string. Finite model theory also studies finite restrictions of logic, such as first-order logic with only a fixed limit of k variables as well as hybrid structures, where nonfinite structures are embedded in finite ones.
Basics
Basically FMT is about the discrimination of structures, i.e. can a set of structures be uniquely described in a certain language. We will see that this can be achieved in FO for a single structures always, for a finite set of structures sometimes and for a set containing infinite structures never.Single Structure
Is a Language L expressive enough to describe a single finite Structure S uniquely (up to isomorphy)?Problem
Given a structure like (1). This structure can be described by FO sentences 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:
Now do these properties describe the structure uniquely (up to isomorphism)? Obviously not since for structure (1') the above properties hold as well.
Simply put, the question is, if one adds enough properties, is it possible that these properties (all together) describe exactly (1) and are valid (all together) for no other structure (up to isomorphy).
Approach
For a single finite structure this is always possible. The principle is quite simple (here for single binary Relations and without constants):- say that there are at least n elements:
- say that there are at most n elements:
- state every element of the Relation R:
- state every non-element of the Relation R:
all for the same tuple
, i.e. .Moreover
This can easily be extended for any fixed number of structures. For, say 2, structures a unique description can easily be obtained by disjunction of the single descriptions, i.e.Writing down a sequence of, say 67, descriptions is easy in theory, but quite impractical. This is a well known problem from programming, where one would use a for loop from 1 to 67 instead. This isn't dealt with in depth here, but mentioned to show that there are more issues to a language than just its expressiveness.
Finite Number of Structures
Is a Language L expressive enough to describe exactly those finite structures that have certain property P in common (up to isomorphy)?Problem
The descriptions so far had in common that they strictly define the number of elements of the universe. Unfortunately most of the 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
The next best thing to a general statement, that we cannot make here, is to give a methodology to differentiate between structures that can and cannot be discriminated.1. The core idea is that whenever one wants to see if a Property P can be expressed in FO, one chooses Structures A and B, where A does have P and B doesn't. If for A and B the same FO sentences hold P cannot be expressed in FO (else it can). For short:
A ∈ P, B ∉ P and A ≡ B
where A ≡ B is A |= α ⇔ B |= α for all FO-sentences α, and P is the class of Structures with property P.
2. The actual methodology partitions the language, like FO, into countably many classes FO[m], such that for each m the above (core idea) has to be shown. That is:
A ∈ P, B ∉ P and A ≡m B
with a pair A, B for each m and α (in ≡) from FO[m].
3. A partition FO[m] can be obtained by the quantifier rank qr(α) of a FO formula α. It expresses the depth of quantifier nesting. For example for a formula in prenex normal form
Prenex normal form
A formula of the predicate calculus is in prenex normal form if it is written as a string of quantifiers followed by a quantifier-free part .Every formula in classical logic is equivalent to a formula in prenex normal form...
qr gives simply the total number of its quantifiers. So FO[m] is defined as all FO formulas α with qr(α) ≤ m.
4. Thus it all comes down to show A |= α ⇔ B |= α on the partitions FO[m]. The main approach here is to use the algebraic characterization provided by Ehrenfeucht-Fraisse Games. What they do is roughly, take a single partial isomorphism on A and B and extend it m times, in order to either prove or disprove A ≡m B, dependent on who wins the game.
Example
We want to show that the property that a structures's size is even can not be expressed on orderered structures A=(A, ≤) by a FO expression.1. Therefore we start with 2 ordered structures A2 and B with universes A2 = {1, 2, 3, 4} and B2 = {1, 2, 3, 4, 5}. Obviously A2 ∈ EVEN and B2 ∉ EVEN, where EVEN is the class of all structures of even size. Now we can show that in a 2-move Ehrenfeucht Fraisse Game (i.e. m = 2, what explains the subscrpts above) on A2 and B2 the duplicator always wins, and thus A2 and B2 cannot be discriminated in FO[2], i.e. A2 |= FO[2] ⇔ B2 |= FO[2].
2. Next we have to scale the structures up by increasing m. For m = 3 we must find an A3 and B3 s.t. the duplicator wins the game. This can be achieved by A3 = {1, ..., 8} and B3 = {1, ..., 9}.
3. More general we choose Am = {1, ..., 2m} and Bm = {1, ..., 2m+1} where we can prove that the duplicator always wins. Thus EVEN on finite ordered structures cannot be expressed in FO qed.
Moreover
An infinite number of structures can only be achieved by allowing structures of infinite size. Thus this is, by definition, no issue of FMT, but for the sake of understanding we consider this case here briefly. We had single structures, that can always be discriminated in FO. We had finite numbers of structures, that in some cases can be discriminated in FO in some cases not. Now for infinite structures, we can never discriminate a structure in FO, i.e. for every infinite model a non-isomorphic one can be found, having exactly the same properties in FO.The most famous example is probably Skolem's theorem: there is a countable non-standard model of arithmetic.
Database Theory
Think of an online-forum. It consists of postings that can have child postings answering them. All together this forms a tree structure with the forum main page seen as a root posting. Thus we have a table "posting" with a relation "answers" from posting to posting. Here all answers of a posting with id "1234" can easily be queried as follows:SELECT *
FROM posting
WHERE posting.answers = '1234';
To obtain the children and grandchildren of "1234" we write:
SELECT * FROM posting
WHERE posting.answers = '1234' OR posting.answers =
(
SELECT id FROM posting
WHERE posting.answers = '1234';
)
For a fixed number of generations this can be extended in SQL (although writing a query for 67 generations is not really a nice job). However we don't know how long a single thread can get. All we know is it must be of finite length. This cannot be expressed in the SQL expressions used above. Therefore we need an extension such as "START WITH ... CONNECT BY ...":
SELECT * FROM posting
START WITH posting.id = '1234'
CONNECT BY PRIOR posting.id = posting.answers;
All the above correspond to logic expressions. The 1st and 2nd query can be expressed in FO, whereas the 3rd query requires some extension like fixed-point-logics.
answers( x, 1234 )
answers( x, 1234 ) ∨ ∃y ( answers( x, y ) ∧ answers( y, 1234 ) )
...
History
- Trakhtenbrot 1950Trakhtenbrot's theoremIn logic and finite model theory, Trakhtenbrot's theorem states that the problem of validity in the class of all finite models is undecidable. In fact, the class of valid sentences over finite models is not recursively enumerable .- References :* Boolos, Burgess, Jeffrey...
: failure of completeness theorem in FO, - Scholz 1952: characterisation of spectra in FO,
- Fagin 1974Fagin's theoremFagin's theorem is a result in descriptive complexity theory that states that the set of all properties expressible in existential second-order logic is precisely the complexity class NP...
: the set of all properties expressible in existential second-order logic is precisely the complexity class NP, - Chandra, Harel 1979/ 80: fixed-point FO extension for db query languages capable of expressing transitive closure -> queries as central objects of FMT.
- ImmermanNeil ImmermanNeil Immerman is an American theoretical computer scientist, a professor of computer science at the University of Massachusetts Amherst...
, 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"
- AbiteboulSerge AbiteboulSerge Joseph Abiteboul is a computer scientist working in the areas of data management, database theory, and finite model theory.He received his PhD from the University of Southern California under the supervision of Seymour Ginsburg, in 1982....
, Hull, Vianu 1995: Book "Foundations of Databases" - ImmermanNeil ImmermanNeil Immerman is an American theoretical computer scientist, a professor of computer science at the University of Massachusetts Amherst...
1999: Book "Descriptive Complexity" - Kuper, Libkin, Paredaens 2000: Book "Constraint Databases"
- Darmstadt 2005/ Aachen2006: first international workshops on "Algorithmic Model Theory"
External links
- R. Fagin. Finite model theory-a personal perspective. Theoretical Computer Science 116, 1993, pp. 3–31.
- Leonid Libkin: The finite model theory toolbox of a database theoretician Also very suitable as general introduction and overview.
- Leonid Libkin: Intro chapter of "Elements of Finite Model Theory". Motivation of 3 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-1994.
- Anju Dawar Infinite and Finite Model Theory, Slides, Uni Cambridge 2002
- 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