Finite Model Theory (FMT) 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 ultraproducts 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"^[1] 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."^[2]

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.

Basics[link]

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.

Characterisation of a Single Structure[link]

Is a Language L expressive enough to describe a single finite Structure S uniquely (up to isomorphy)?

Problem[link]

Given a structure like (1). This structure can be described by FO sentences like

1. every node has an edge to another node: Failed to parse (Missing texvc executable; please see math/README to configure.): \forall_x \exists_y G(x, y).

1. no node has an edge to itself: Failed to parse (Missing texvc executable; please see math/README to configure.): \forall_{x,y} (G(x, y) \Rightarrow x \neq y).

1. there is at least one node that is connected to all others: Failed to parse (Missing texvc executable; please see math/README to configure.): \exists_x \forall_y (x \neq y \Rightarrow G(x, y)).

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[link]

For a single finite structure this is always possible. The principle is quite simple (here for single binary Relations and without constants):

1. say that there are at least n elements: Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi_1 = \bigwedge_{i\ne j} \neg x_i = x_j

1. say that there are at most n elements: Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi_2 = \forall_y \bigvee_{i} x_i = y

1. state every element of the Relation R: Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi_3 = \bigwedge_{(a_i, a_j) \in R} R(x_i, x_j)

1. state every non-element of the Relation R: Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi_4 = \bigwedge_{(a_i, a_j) \notin R} \neg R(x_i, x_j)

all for the same tuple Failed to parse (Missing texvc executable; please see math/README to configure.): x_1 .. x_n , i.e. Failed to parse (Missing texvc executable; please see math/README to configure.): \exists_{x_1} ... \exists_{x_n} (\varphi_1 \land \varphi_2 \land \varphi_3 \land \varphi_4) .

Extension to a fixed Number of Structures[link]

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.

Failed to parse (Missing texvc executable; please see math/README to configure.): \exists_{x_1} ... \exists_{x_n} (\varphi_1 \land \varphi_2 \land \varphi_3 \land \varphi_4) \lor \exists_{x_1} ... \exists_{x_n} (\varrho_1 \land \varrho_2 \land \varrho_3 \land \varrho_4)

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.

Extension to an infinite Structure[link]

This is, by definition, no issue of FMT, but for the sake of understanding we consider this case here briefly. Infinite structures, can never be discriminated 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.

Characterisation of a Class of Structures[link]

Is a Language L expressive enough to describe exactly those finite structures that have certain property P in common (up to isomorphy)?

Set of up to n structures.

Problem[link]

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[link]

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 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[link]

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

1. The idea is to pick A ∈ EVEN and B ∉ EVEN, where EVEN is the class of all structures of even size.

2. Therefore we start with 2 ordered structures A₂ and B₂ with universes A₂ = {1, 2, 3, 4} and B₂ = {1, 2, 3, 4, 5}. Obviously A₂ ∈ EVEN and B₂ ∉ EVEN.

3. Now we can show* that in a 2-move Ehrenfeucht-Fraisse Game (i.e. m = 2, what explains the subscrpts above) on A₂ and B₂ the duplicator always wins, and thus A₂ and B₂ cannot be discriminated in FO[2], i.e. A₂ |= FO[2] ⇔ B₂ |= FO[2].

4. Next we have to scale the structures up by increasing m. For example for m = 3 we must find an A₃ and B₃ s.t. the duplicator wins the game. This can be achieved by A₃ = {1, ..., 8} and B₃ = {1, ..., 9}. More general, we choose A_m = {1, ..., 2^m} and B_m = {1, ..., 2^m+1} where we can prove that the duplicator always wins*. Thus EVEN on finite ordered structures cannot be expressed in FO, qed.

(*) Notice that the proof of the result of the Ehrenfeucht-Fraisse Game has been omitted, since it is not the main focus here.

Applications[link]

Database Theory[link]

SQL is based on First Order Logic (FO), 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 X LAST_NAME. The FO query G('Judy', l), which returns all the last names where the first name is 'Judy', would look in SQL like this:

select LAST_NAME 
from GIRLS
where FIRST_NAME = 'Judy'

Notice, we assume here, that all last names appear only once.

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 last names of all the gils that have the same last name as at least one of the boys. In FO this is ∃_h( G(f, l) ∧ B(h, l) ). The corresponding SQL statement is:

select FIRST_NAME, LAST_NAME 
from GIRLS
where LAST_NAME IN ( selcet LAST_NAME from BOYS )

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.

Querying & Search[link]

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

("Java" OR ("C#" AND NOT "note")) AND ("Oracle" OR "Microsoft")

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

History[link]

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

References[link]

1. ^ Fagin, Ronald (1993). Finite model theory-a personal perspective. 
2. ^ Immerman, Neil (1999). Descriptive Complexity. New York: Springer-Verlag. p. 6. ISBN 0-387-98600-6. 

External links[link]

Wikibooks has a book on the topic of Finite Model Theory

• 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.
• Anuj 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
• Ebbinghaus, H.-D. (1995). Finite Model Theory. Berlin Heidelberg: Springer. ISBN 3-540-65758-4. 

In mathematics, model theory is the study of (classes of) mathematical structures (e.g. groups, fields, graphs, universes of set theory) using tools from mathematical logic. It has close ties to abstract algebra, particularly universal algebra.

Objects of study in model theory are models for formal languages which are structures that give meaning to the sentences of these formal languages. If a model for a language moreover satisfies a particular sentence or theory (set of sentences satisfying special conditions), it is called a model of the sentence or theory.

This article focuses on finitary first order model theory of infinite structures. Finite model theory, which concentrates on finite structures, diverges significantly from the study of infinite structures in both the problems studied and the techniques used. Model theory in higher-order logics or infinitary logics is hampered by the fact that completeness does not in general hold for these logics. However, a great deal of study has also been done in such languages.

Introduction[link]

Model theory recognises and is intimately concerned with a duality: It examines semantical elements by means of syntactical elements of a corresponding language. To quote the first page of Chang and Keisler (1990):^[1]

universal algebra + logic = model theory.

Model theory developed rapidly during the 1990s, and a more modern definition is provided by Wilfrid Hodges (1997):

model theory = algebraic geometry − fields.

In a similar way to proof theory, model theory is situated in an area of interdisciplinarity between mathematics, philosophy, and computer science. The most important professional organization in the field of model theory is the Association for Symbolic Logic.

An incomplete and somewhat arbitrary subdivision of model theory is into classical model theory, model theory applied to groups and fields, and geometric model theory. A missing subdivision is computable model theory, but this can arguably be viewed as an independent subfield of logic. Examples of early theorems from classical model theory include Gödel's completeness theorem, the upward and downward Löwenheim–Skolem theorems, Vaught's two-cardinal theorem, Scott's isomorphism theorem, the omitting types theorem, and the Ryll-Nardzewski theorem. Examples of early results from model theory applied to fields are Tarski's elimination of quantifiers for real closed fields, Ax's theorem on pseudo-finite fields, and Robinson's development of non-standard analysis. An important step in the evolution of classical model theory occurred with the birth of stability theory (through Morley's theorem on uncountably categorical theories and Shelah's classification program), which developed a calculus of independence and rank based on syntactical conditions satisfied by theories. During the last several decades applied model theory has repeatedly merged with the more pure stability theory. The result of this synthesis is called geometric model theory in this article (which is taken to include o-minimality, for example, as well as classical geometric stability theory). An example of a theorem from geometric model theory is Hrushovski's proof of the Mordell–Lang conjecture for function fields. The ambition of geometric model theory is to provide a geography of mathematics by embarking on a detailed study of definable sets in various mathematical structures, aided by the substantial tools developed in the study of pure model theory.

Example[link]

To illustrate the basic relationship involving syntax and semantics in the context of a non-trivial model, one can start, on the syntactic side, with suitable axioms for the natural numbers such as Peano axioms, and the associated theory. Going on to the semantic side, one has the usual counting numbers as a model. In the 1930s, Skolem developed alternative models satisfying the axioms. This illustrates what is meant by interpreting a language or theory in a particular model. A more traditional example is interpreting the axioms of a particular algebraic system such as a group, in the context of a model provided by a specific group.

Universal algebra[link]

Fundamental concepts in universal algebra are signatures σ and σ-algebras. Since these concepts are formally defined in the article on structures, the present article can content itself with an informal introduction which consists in examples of how these terms are used.

The standard signature of rings is σ_ring = {×,+,−,0,1}, where × and + are binary, − is unary, and 0 and 1 are nullary.

The standard signature of semirings is σ_smr = {×,+,0,1}, where the arities are as above.

The standard signature of groups (with multiplicative notation) is σ_grp = {×,⁻¹,1}, where × is binary, ⁻¹ is unary and 1 is nullary.

The standard signature of monoids is σ_mnd = {×,1}.

A ring is a σ_ring-structure which satisfies the identities u + (v + w) = (u + v) + w, u + v = v + u, u + 0 = u, u + (−u) = 0, u × (v × w) = (u × v) × w, u × 1 = u, 1 × u = u, u × (v + w) = (u × v) + (u × w) and (v + w) × u = (v × u) + (w × u).

A group is a σ_grp-structure which satisfies the identities u × (v × w) = (u × v) × w, u × 1 = u, 1 × u = u, u × u⁻¹ = 1 and u⁻¹ × u = 1.

A monoid is a σ_mnd-structure which satisfies the identities u × (v × w) = (u × v) × w, u × 1 = u and 1 × u = u.

A semigroup is a {×}-structure which satisfies the identity u × (v × w) = (u × v) × w.

A magma is just a {×}-structure.

This is a very efficient way to define most classes of algebraic structures, because there is also the concept of σ-homomorphism, which correctly specializes to the usual notions of homomorphism for groups, semigroups, magmas and rings. For this to work, the signature must be chosen well.

Terms such as the σ_ring-term t(u,v,w) given by (u + (v × w)) + (−1) are used to define identities t = t', but also to construct free algebras. An equational class is a class of structures which, like the examples above and many others, is defined as the class of all σ-structures which satisfy a certain set of identities. Birkhoff's theorem states:

A class of σ-structures is an equational class if and only if it is not empty and closed under subalgebras, homomorphic images, and direct products.

An important non-trivial tool in universal algebra are ultraproducts Failed to parse (Missing texvc executable; please see math/README to configure.): \Pi_{i\in I}A_i/U , where I is an infinite set indexing a system of σ-structures A_i, and U is an ultrafilter on I.

While model theory is generally considered a part of mathematical logic, universal algebra, which grew out of Alfred North Whitehead's (1898) work on abstract algebra, is part of algebra. This is reflected by their respective MSC classifications. Nevertheless model theory can be seen as an extension of universal algebra.

Finite model theory[link]

Finite model theory is the area of model theory which has the closest ties to universal algebra. Like some parts of universal algebra, and in contrast with the other areas of model theory, it is mainly concerned with finite algebras, or more generally, with finite σ-structures for signatures σ which may contain relation symbols as in the following example:

The standard signature for graphs is σ_grph={E}, where E is a binary relation symbol.

A graph is a σ_grph-structure satisfying the sentences Failed to parse (Missing texvc executable; please see math/README to configure.): \forall u \forall v(uEv \rightarrow vEu)

and Failed to parse (Missing texvc executable; please see math/README to configure.): \forall u\neg(uEu)

.

A σ-homomorphism is a map that commutes with the operations and preserves the relations in σ. This definition gives rise to the usual notion of graph homomorphism, which has the interesting property that a bijective homomorphism need not be invertible. Structures are also a part of universal algebra; after all, some algebraic structures such as ordered groups have a binary relation <. What distinguishes finite model theory from universal algebra is its use of more general logical sentences (as in the example above) in place of identities. (In a model-theoretic context an identity t=t' is written as a sentence Failed to parse (Missing texvc executable; please see math/README to configure.): \forall u_1u_2\dots u_n(t=t') .)

The logics employed in finite model theory are often substantially more expressive than first-order logic, the standard logic for model theory of infinite structures.

First-order logic[link]

Whereas universal algebra provides the semantics for a signature, logic provides the syntax. With terms, identities and quasi-identities, even universal algebra has some limited syntactic tools; first-order logic is the result of making quantification explicit and adding negation into the picture.

A first-order formula is built out of atomic formulas such as R(f(x,y),z) or y = x + 1 by means of the Boolean connectives Failed to parse (Missing texvc executable; please see math/README to configure.): \neg,\land,\lor,\rightarrow

and prefixing of quantifiers Failed to parse (Missing texvc executable; please see math/README to configure.): \forall v
or Failed to parse (Missing texvc executable; please see math/README to configure.): \exists v

. A sentence is a formula in which each occurrence of a variable is in the scope of a corresponding quantifier. Examples for formulas are φ (or φ(x) to mark the fact that at most x is an unbound variable in φ) and ψ defined as follows:

Failed to parse (Missing texvc executable; please see math/README to configure.): {\varphi \;=\; \forall u\forall v(\exists w (x\times w=u\times v)\rightarrow(\exists w(x\times w=u)\lor\exists w(x\times w=v)))\land x\ne 0\land x\ne1,}

Failed to parse (Missing texvc executable; please see math/README to configure.): \psi \;=\; \forall u\forall v((u\times v=x)\rightarrow (u=x)\lor(v=x))\land x\ne 0\land x\ne1.

(Note that the equality symbol has a double meaning here.) It is intuitively clear how to translate such formulas into mathematical meaning. In the σ_smr-structure Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal N

of the natural numbers, for example, an element n satisfies the formula φ if and only if n is a prime number. The formula ψ similarly defines irreducibility. Tarski gave a rigorous definition, sometimes called "Tarski's definition of truth", for the satisfaction relation Failed to parse (Missing texvc executable; please see math/README to configure.): \models

, so that one easily proves:

Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal N\models\phi(n) \iff n

is a prime number.

Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal N\models\psi(n) \iff n

is irreducible.

A set T of sentences is called a (first-order) theory. A theory is satisfiable if it has a model Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal M\models T , i.e. a structure (of the appropriate signature) which satisfies all the sentences in the set T. Consistency of a theory is usually defined in a syntactical way, but in first-order logic by the completeness theorem there is no need to distinguish between satisfiability and consistency. Therefore model theorists often use "consistent" as a synonym for "satisfiable".

A theory is called categorical if it determines a structure up to isomorphism, but it turns out that this definition is not useful, due to serious restrictions in the expressivity of first-order logic. The Löwenheim–Skolem theorem implies that for every theory T^[2] which has an infinite model and for every infinite cardinal number κ, there is a model Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal M\models T

such that the number of elements of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal M
is exactly κ. Therefore only finite structures can be described by a categorical theory.

Lack of expressivity (when compared to higher logics such as second-order logic) has its advantages, though. For model theorists, the Löwenheim–Skolem theorem is an important practical tool rather than the source of Skolem's paradox. In a certain sense made precise by Lindström's theorem, first-order logic is the most expressive logic for which both the Löwenheim–Skolem theorem and the compactness theorem hold.

Due to Gödel, the compactness theorem says that every unsatisfiable first-order theory has a finite unsatisfiable subset. This theorem is of central importance in infinite model theory, where the words "by compactness" are commonplace. One way to prove it is by means of ultraproducts. An alternative proof uses the completeness theorem, which is otherwise reduced to a marginal role in most of modern model theory.

Axiomatizability, elimination of quantifiers, and model-completeness[link]

The first step, often trivial, for applying the methods of model theory to a class of mathematical objects such as groups, or trees in the sense of graph theory, is to choose a signature σ and represent the objects as σ-structures. The next step is to show that the class is an elementary class, i.e. axiomatizable in first-order logic (i.e. there is a theory T such that a σ-structure is in the class if and only if it satisfies T). E.g. this step fails for the trees, since connectedness cannot be expressed in first-order logic. Axiomatizability ensures that model theory can speak about the right objects. Quantifier elimination can be seen as a condition which ensures that model theory does not say too much about the objects.

A theory T has quantifier elimination if every first-order formula φ(x₁,...,x_n) over its signature is equivalent modulo T to a first-order formula ψ(x₁,...,x_n) without quantifiers, i.e. Failed to parse (Missing texvc executable; please see math/README to configure.): \forall x_1\dots\forall x_n(\phi(x_1,\dots,x_n)\leftrightarrow \psi(x_1,\dots,x_n))

holds in all models of T. For example the theory of algebraically closed fields in the signature σring=(×,+,−,0,1) has quantifier elimination because every formula is equivalent to a Boolean combination of equations between polynomials.

A substructure of a σ-structure is a subset of its domain, closed under all functions in its signature σ, which is regarded as a σ-structure by restricting all functions and relations in σ to the subset. An embedding of a σ-structure Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal A

into another σ-structure Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal B
is a map f: A → B between the domains which can be written as an isomorphism of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal A
with a substructure of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal B

. Every embedding is an injective homomorphism, but the converse holds only if the signature contains no relation symbols.

If a theory does not have quantifier elimination, one can add additional symbols to its signature so that it does. Early model theory spent much effort on proving axiomatizability and quantifier elimination results for specific theories, especially in algebra. But often instead of quantifier elimination a weaker property suffices:

A theory T is called model-complete if every substructure of a model of T which is itself a model of T is an elementary substructure. There is a useful criterion for testing whether a substructure is an elementary substructure, called the Tarski–Vaught test. It follows from this criterion that a theory T is model-complete if and only if every first-order formula φ(x₁,...,x_n) over its signature is equivalent modulo T to an existential first-order formula, i.e. a formula of the following form:

Failed to parse (Missing texvc executable; please see math/README to configure.): \exists v_1\dots\exists v_m\psi(x_1,\dots,x_n,v_1,\dots,v_m)

, where ψ is quantifier free. A theory that is not model-complete may or may not have a model completion, which is a related model-complete theory that is not, in general, an extension of the original theory. A more general notion is that of model companions.

Categoricity[link]

As observed in the section on first-order logic, first-order theories cannot be categorical, i.e. they cannot describe a unique model up to isomorphism, unless that model is finite. But two famous model-theoretic theorems deal with the weaker notion of κ-categoricity for a cardinal κ. A theory T is called κ-categorical if any two models of T that are of cardinality κ are isomorphic. It turns out that the question of κ-categoricity depends critically on whether κ is bigger than the cardinality of the language (i.e. Failed to parse (Missing texvc executable; please see math/README to configure.): \aleph_0  + |σ|, where |σ| is the cardinality of the signature). For finite or countable signatures this means that there is a fundamental difference between Failed to parse (Missing texvc executable; please see math/README to configure.): \aleph_0 -cardinality and κ-cardinality for uncountable κ.

A few characterizations of Failed to parse (Missing texvc executable; please see math/README to configure.): \aleph_0 -categoricity include:

For a complete first-order theory T in a finite or countable signature the following conditions are equivalent:

1. T is Failed to parse (Missing texvc executable; please see math/README to configure.): \aleph_0

-categorical.

1. For every natural number n, the Stone space S_n(T) is finite.
2. For every natural number n, the number of formulas φ(x₁, ..., x_n) in n free variables, up to equivalence modulo T, is finite.

This result, due independently to Engeler, Ryll-Nardzewski and Svenonius, is sometimes referred to as the Ryll-Nardzewski theorem.

Further, Failed to parse (Missing texvc executable; please see math/README to configure.): \aleph_0 -categorical theories and their countable models have strong ties with oligomorphic groups. They are often constructed as Fraïssé limits.

Michael Morley's highly non-trivial result that (for countable languages) there is only one notion of uncountable categoricity was the starting point for modern model theory, and in particular classification theory and stability theory:

Morley's categoricity theorem

If a first-order theory T in a finite or countable signature is κ-categorical for some uncountable cardinal κ, then T is κ-categorical for all uncountable cardinals κ.

Uncountably categorical (i.e. κ-categorical for all uncountable cardinals κ) theories are from many points of view the most well-behaved theories. A theory that is both Failed to parse (Missing texvc executable; please see math/README to configure.): \aleph_0 -categorical and uncountably categorical is called totally categorical.

Model theory and set theory[link]

Set theory (which is expressed in a countable language), if it is consistent, has a countable model; this is known as Skolem's paradox, since there are sentences in set theory which postulate the existence of uncountable sets and yet these sentences are true in our countable model. Particularly the proof of the independence of the continuum hypothesis requires considering sets in models which appear to be uncountable when viewed from within the model, but are countable to someone outside the model.

The model-theoretic viewpoint has been useful in set theory; for example in Kurt Gödel's work on the constructible universe, which, along with the method of forcing developed by Paul Cohen can be shown to prove the (again philosophically interesting) independence of the axiom of choice and the continuum hypothesis from the other axioms of set theory.

Other basic notions of model theory[link]

Reducts and expansions[link]

A field or a vector space can be regarded as a (commutative) group by simply ignoring some of its structure. The corresponding notion in model theory is that of a reduct of a structure to a subset of the original signature. The opposite relation is called an expansion - e.g. the (additive) group of the rational numbers, regarded as a structure in the signature {+,0} can be expanded to a field with the signature {×,+,1,0} or to an ordered group with the signature {+,0,<}.

Similarly, if σ' is a signature that extends another signature σ, then a complete σ'-theory can be restricted to σ by intersecting the set of its sentences with the set of σ-formulas. Conversely, a complete σ-theory can be regarded as a σ'-theory, and one can extend it (in more than one way) to a complete σ'-theory. The terms reduct and expansion are sometimes applied to this relation as well.

Interpretability[link]

Given a mathematical structure, there are very often associated structures which can be constructed as a quotient of part of the original structure via an equivalence relation. An important example is a quotient group of a group.

One might say that to understand the full structure one must understand these quotients. When the equivalence relation is definable, we can give the previous sentence a precise meaning. We say that these structures are interpretable.

A key fact is that one can translate sentences from the language of the interpreted structures to the language of the original structure. Thus one can show that if a structure M interprets another whose theory is undecidable, then M itself is undecidable.

Using the compactness and completeness theorems[link]

Gödel's completeness theorem (not to be confused with his incompleteness theorems) says that a theory has a model if and only if it is consistent, i.e. no contradiction is proved by the theory. This is the heart of model theory as it lets us answer questions about theories by looking at models and vice-versa. One should not confuse the completeness theorem with the notion of a complete theory. A complete theory is a theory that contains every sentence or its negation. Importantly, one can find a complete consistent theory extending any consistent theory. However, as shown by Gödel's incompleteness theorems only in relatively simple cases will it be possible to have a complete consistent theory that is also recursive, i.e. that can be described by a recursively enumerable set of axioms. In particular, the theory of natural numbers has no recursive complete and consistent theory. Non-recursive theories are of little practical use, since it is undecidable if a proposed axiom is indeed an axiom, making proof-checking a supertask.

The compactness theorem states that a set of sentences S is satisfiable if every finite subset of S is satisfiable. In the context of proof theory the analogous statement is trivial, since every proof can have only a finite number of antecedents used in the proof. In the context of model theory, however, this proof is somewhat more difficult. There are two well known proofs, one by Gödel (which goes via proofs) and one by Malcev (which is more direct and allows us to restrict the cardinality of the resulting model).

Model theory is usually concerned with first-order logic, and many important results (such as the completeness and compactness theorems) fail in second-order logic or other alternatives. In first-order logic all infinite cardinals look the same to a language which is countable. This is expressed in the Löwenheim–Skolem theorems, which state that any countable theory with an infinite model Failed to parse (Missing texvc executable; please see math/README to configure.): \mathfrak{A}

has models of all infinite cardinalities (at least that of the language) which agree with Failed to parse (Missing texvc executable; please see math/README to configure.): \mathfrak{A}
on all sentences, i.e. they are 'elementarily equivalent'.

Types[link]

Fix an Failed to parse (Missing texvc executable; please see math/README to configure.): L -structure Failed to parse (Missing texvc executable; please see math/README to configure.): M , and a natural number Failed to parse (Missing texvc executable; please see math/README to configure.): n . The set of definable subsets of Failed to parse (Missing texvc executable; please see math/README to configure.): M^n

over some parameters Failed to parse (Missing texvc executable; please see math/README to configure.): A
is a Boolean algebra. By Stone's representation theorem for Boolean algebras there is a natural dual notion to this. One can consider this to be the topological space consisting of maximal consistent sets of formulae over Failed to parse (Missing texvc executable; please see math/README to configure.): A

. We call this the space of (complete) Failed to parse (Missing texvc executable; please see math/README to configure.): n -types over Failed to parse (Missing texvc executable; please see math/README to configure.): A , and write Failed to parse (Missing texvc executable; please see math/README to configure.): S_n(A) .

Now consider an element Failed to parse (Missing texvc executable; please see math/README to configure.): m \in M^n . Then the set of all formulae Failed to parse (Missing texvc executable; please see math/README to configure.): \phi

with parameters in Failed to parse (Missing texvc executable; please see math/README to configure.): A
in free variables Failed to parse (Missing texvc executable; please see math/README to configure.): x_1,\ldots,x_n
so that Failed to parse (Missing texvc executable; please see math/README to configure.): M \models \phi(m)
is consistent and maximal such. It is called the type of Failed to parse (Missing texvc executable; please see math/README to configure.): m
over Failed to parse (Missing texvc executable; please see math/README to configure.): A

.

One can show that for any Failed to parse (Missing texvc executable; please see math/README to configure.): n -type Failed to parse (Missing texvc executable; please see math/README to configure.): p , there exists some elementary extension Failed to parse (Missing texvc executable; please see math/README to configure.): N

of Failed to parse (Missing texvc executable; please see math/README to configure.): M
and some Failed to parse (Missing texvc executable; please see math/README to configure.): a \in N^n
so that Failed to parse (Missing texvc executable; please see math/README to configure.): p
is the type of Failed to parse (Missing texvc executable; please see math/README to configure.): a
over Failed to parse (Missing texvc executable; please see math/README to configure.): A

.

Many important properties in model theory can be expressed with types. Further many proofs go via constructing models with elements that contain elements with certain types and then using these elements.

Illustrative Example: Suppose Failed to parse (Missing texvc executable; please see math/README to configure.): M

is an algebraically closed field. The theory has quantifier elimination . This allows us to show that a type is determined exactly by the polynomial equations it contains. Thus the space of Failed to parse (Missing texvc executable; please see math/README to configure.): n

-types over a subfield Failed to parse (Missing texvc executable; please see math/README to configure.): A

is bijective with the set of prime ideals of the polynomial ring Failed to parse (Missing texvc executable; please see math/README to configure.): A[x_1,\ldots,x_n]

. This is the same set as the spectrum of Failed to parse (Missing texvc executable; please see math/README to configure.): A[x_1,\ldots,x_n] . Note however that the topology considered on the type space is the constructible topology: a set of types is basic open iff it is of the form Failed to parse (Missing texvc executable; please see math/README to configure.): \{p: f(x)=0 \in p\}

or of the form Failed to parse (Missing texvc executable; please see math/README to configure.): \{p: f(x) \neq 0 \in p\}

. This is finer than the Zariski topology.

Early history[link]

Model theory as a subject has existed since approximately the middle of the 20th century. However some earlier research, especially in mathematical logic, is often regarded as being of a model-theoretical nature in retrospect. The first significant result in what is now model theory was a special case of the downward Löwenheim–Skolem theorem, published by Leopold Löwenheim in 1915. The compactness theorem was implicit in work by Thoralf Skolem,^[3] but it was first published in 1930, as a lemma in Kurt Gödel's proof of his completeness theorem. The Löwenheim–Skolem theorem and the compactness theorem received their respective general forms in 1936 and 1941 from Anatoly Maltsev.

See also[link]

Notes[link]

References[link]

Canonical textbooks[link]

• Chang, Chen Chung; Keisler, H. Jerome (1990) [1973]. Model Theory. Studies in Logic and the Foundations of Mathematics (3rd ed.). Elsevier. ISBN 978-0-444-88054-3 
• Hodges, Wilfrid (1997). A shorter model theory. Cambridge: Cambridge University Press. ISBN 978-0-521-58713-6 
• Marker, David (2002). Model Theory: An Introduction. Graduate Texts in Mathematics 217. Springer. ISBN 0-387-98760-6. 

Other textbooks[link]

• Bell, John L.; Slomson, Alan B. (2006) [1969]. Models and Ultraproducts: An Introduction (reprint of 1974 ed.). Dover Publications. ISBN 0-486-44979-3. 
• Ebbinghaus, Heinz-Dieter; Flum, Jörg; Thomas, Wolfgang (1994). Mathematical Logic. Springer. ISBN 0-387-94258-0. 
• Hinman, Peter G. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0. 
• Manzano, Maria (1989). Teoria de modelos. Alianza editorial. ISBN 84-206-8126-1. 
• Hodges, Wilfrid (1993). Model theory. Cambridge University Press. ISBN 0-521-30442-3. 
• Manzano, Maria (1999). Model theory. Oxford University Press. ISBN 0-19-853851-0. 
• Poizat, Bruno (2000). A Course in Model Theory. Springer. ISBN 0-387-98655-3. 
• Rautenberg, Wolfgang (2010). A Concise Introduction to Mathematical Logic (3rd ed.). New York: Springer Science+Business Media. DOI:10.1007/978-1-4419-1221-3. ISBN 978-1-4419-1220-6. http://www.springerlink.com/content/978-1-4419-1220-6/. 
• Rothmaler, Philipp (2000). Introduction to Model Theory (new ed.). Taylor & Francis. ISBN 90-5699-313-5. 

Free online texts[link]

• Chatzidakis, Zoe (2001). Introduction to Model Theory. pp. 26 pages in DVI format. http://www.logique.jussieu.fr/~zoe/papiers/MTluminy.dvi. 
• Pillay, Anand (2002). Lecture Notes – Model Theory. pp. 61 pages. http://www.math.uiuc.edu/People/pillay/lecturenotes_modeltheory.pdf. 
• Hodges, Wilfrid, First-order Model theory. The Stanford Encyclopedia Of Philosophy, E. Zalta (ed.).
• Simmons, Harold (2004), An introduction to Good old fashioned model theory. Notes of an introductory course for postgraduates (with exercises).
• J. Barwise and S. Feferman (editors), Model-Theoretic Logics, Perspectives in Mathematical Logic, Volume 8, New York: Springer-Verlag, 1985.

Benjamin Schumacher is a U.S. theoretical physicist, working mostly in the field of quantum information theory.^[2]

He discovered a way of interpreting quantum states as information. He came up with a way of compressing the information in a state, and storing the information in a smaller number of states. This is now known as Schumacher compression. This was the quantum analog of Shannon's noiseless coding theorem, and it helped to start the field known as quantum information theory.

Schumacher is also credited with inventing the term qubit, which is to quantum computation as a bit is to traditional computation.

He is the author of Physics in Spacetime,^[1] a textbook on Special Relativity, and is also a professor at Kenyon College, a small liberal arts college in rural Ohio. Also he holds the lecture on Quantum Mechanics: The Physics of the Microscopic World in The Teaching Company program.^[5]

Schumacher earned his bachelors degree at Hendrix College and his Ph.D. from the University of Texas at Austin.

Influential research papers[link]

• Quantum coding. Phys. Rev. A 51, 2738 - 2747 (1995)

References[link]

External links[link]

• Zeroth Order Approximation - Blog by Benjamin Schumacher
• Benjamin Schumacher Homepage
• Quantum Mechanics: The Physics of the Microscopic World
• The Physics of Impossible Things, Speaker: Ben Schumacher, 03/12/2008, PIRSA - Perimeter Institute Recorded Seminar Archive

This article about an American physicist is a stub. You can help Wikipedia by expanding it. v t e