On the one hand, there is syntax. On the other hand, there is semantics. Model theory is (roughly) about the relations between the two: model theory studies classes of models of theories, hence classes of “mathematical structures”.
A model theory for a particular logic typically works within a given universe, and specifies a notion of “mathematical structure” in this context, namely a structure for a language, and a definition of truth. Logic is typically specified by language (function symbols, relations symbols and constants); formulas (formed from symbols, variables, Boolean operations and quantifiers). Language together with a choice of a set of formulas without free variables (viewed as axioms) is called a theory. A structure is an interpretation of a language via a given set together with interpretation of the symbols of the language. A model of a theory in the language is an L-structure which satisfies each formula in .
The two main problems of model theory are
In all memorable examples, the collection of structures for a language will form an interesting category (see Beke-Rosicky 11 for a characterization of these), and the subcollection of those structures verifying a given collection of propositions in the language are an interesting subcategory again.
Model theory as currently conceived has strong analogies with the classical theory of algebraic varieties and hence with the part of algebraic geometry that deals with these. One such analogy is that definable subsets are likened to zero loci of equations, and another consists of various notions of dimension which can be likened to Krull dimension. One can also say that classical algebraic geometry often provides a testing ground for more general developments in model theory. (For the most part, model theory does not deal however with more global concepts of modern algebraic geometry such as sheaves or schemes.)
In full generality, model theory would study all kinds of models over all kinds of theories, hence pretty much everything that is considered (in) mathematics. However, in order to find effective classification results for models, one traditionally restricts attention to very special kinds of theories only.
Traditionally the default subject of model theory (e.g. (Hodges 93)) are first-order theories (only) and their models in Set (only), these are the traditional structures in model theory. For emphasis the study of this specific case is also called first-order model theory or classical model theory (SEP). Among the fundamental classfication theorems provable in this context are the compactness theorem and the Löwenheim-Skolem theorem. (See also geometric stability theory.)
More modern developments in model theory consider also wider classes of theories than just first-order theories (e.g Tent-Ziegler 12). In particular there is categorical model theory (Makkai-Paré 89, Beke-Rosicky 11).
More generally one can consider models over theories in higher-order logic, this we discuss below in
Caveat Lector. This may duplicate/contradict other nLab accounts of FOL, e.g. theory; it is present here for illustrative purposes only. We attempt to obviate the trouble of quantifier scope by using addressing rather than naming of variables; specifically, the variable occurs bound in a formula if it is nested within more than quantifiers, and otherwise free.
We describe an operad in Set over two types, and for “words” and “propositions”, respectively. The full operad is freely generated by various disjoint suboperads * a free suboperad of operations, or functions, of types ; * an -indexed suboperad of variables of types ; * a (free) suboperad of predicates, or relations, of types ; * the equality operad, of type * the boolean operad, : it’s got of types for , and perhaps if you want to include ; these compose the way you think they should. * the quantifier , usually written , where ; \forall is of type .
Notable subsets of include , generated by , the suboperad of parametrized words, and , the elements of types in the suboperad generated by .
The Tarski Definition of Truth is a natural extension of the -algebra to an -algebra, such that * for in and for all functions , the sensible thing is true in . * is true if for all functions , both and are true, and is true if and only if is not. * is true in precisely when is true for all , where
(Again, this really should be written more clearly, but it’s a start.)
JCMcKeown: is there some nicer way to say the quantifier nonsense? I’m thinking along the lines
there are two actions of on : one shifts all the variables by 1, the other adds a quantifier; and the Tarski extension is the one that makes these commute somehow
ibid: maybe it’s more right to say that should be the boolean algebra ? This again has that natural action of on it…
An -structure , as an -algebra with extra properties, defines a complete first-order theory , that subset of which interprets as , or true. Conversely, given a collection of elements of of type , we say that , or in words is a model of the theory whenever . There is an obvious Galois connection between theories and the collections of -structures that are models. Much of deeper model theory studies the fine structure of this connection.
Structures from universal algebra, higher algebra and categorical logic that conveniently allow tospeak about theories and their models are operads, monads and Lawvere theories. Each of these may be understood as characterizing a theory. Its models then are the corresponging algebras, see at algebra over an operad, algebra over a monad and algebra over a Lawvere theory, respectively.
((insert your favourite variant here))
For a reasonable fragment of infinitary logic, then the category of all models over theories in this language is an accessible category and moreover all accessible categories arise this way. (Makkai-Pare 89, Beke-Rosicky 11).
The following are closely interrelated, and depend on having a suitable universe . We can view them as theorems of or as (relatively mild) conditions on .
(… clarify …)
Given a first-order theory in some language , is consistent iff there is a model of in — that is, iff for some .
See at completeness theorem?.
Under the same hypotheses, is consistent iff every finite subset of is consistent; expressed semantically, a theory has a model iff every finite subset of has a model.
See at compactness theorem.
(…think of a good way to state this…)
It follows that first-order theories are quite permissive; or in other words that they’re inefficient at pinning down particular structures.
For example, consider the complete first-order theory , and any total order . If one expands the language (coresponding to an injective morphism of operads) to include constant symbols for , then for any subset of of finite size , one has
so that the finite extensions of by suborders of are all consistent; by compactness, the fully extended theory is also consistent; thus by completeness there is a structure such that * * for all in
By a similar argument, (if ZFC is consistent) there are models of classical set theory satisfying the (higher-order) property that the natural numbers object of includes your favourite total order as a suborder — of course, isn’t allowed to know this — notably, there is no object in such that .
Discussion of classical first-order model theory includes
Stanford Encyclopedia of Philosophy, First-order Model Theory
Wikipedia, Model theory
Wilfrid Hodges, Model Theory, Cambridge University Press 1993; A shorter model theory, Cambridge UP 1997
Other basic texts on model theory include
Katrin Tent, Martin Ziegler, A course in model theory, Lecture Notes in Logic, Cambridge University Press, April 2012
Chen Chung Chang, H. Jerome Keisler, Model Theory. Studies in Logic and the Foundations of Mathematics. 1973, 1990, Elsevier.
David Marker, Model Theory: An Introduction Graduate Texts in Mathematics 217 (2002)
C U Jensen, H Lenzing, Model theoretic algebra: with particular emphasis on fields, rings, modules (1989)
Gerald E Sacks, Saturated model theory, Benjamin 1972
Specific discussion of generalization of classical first-order model theory to more general kinds of logic include…
…to modal logic:
…to infinitary logic:
B.Hart et. al (eds.), Models, Logics, and Higher-dimensional Categories, A Tribute to the Work of Mihali Makkai, AMS (2011)
Discussion of geometric stability theory includes
Boris Zilber, Elements of geometric stability theory, lecture notes, pdf; On model theory, non-commutative geometry and physics, (survey draft) pdf; Zariski geometries, book, draft pdf; On model theory, noncommutative geometry and physics, conference talk, video
John T. Baldwin, Fundamentals of stability theory
Discussion of motivic integration includes