nLab model theory




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), and 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 LL via a given set MM together with interpretation of the symbols of the language. A model of a theory 𝒯\mathcal{T} in the language LL is an L-structure which satisfies each formula in 𝒯\mathcal{T}.

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


Classical model theory is concerned with models of theories in first-order logic, this is what we discuss first, below in

More generally one can consider models over theories in higher-order logic, this we discuss below in

Classical Model theory in First-order logic

See also/first theory/first-order theory.

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 x nx_n occurs bound in a formula if it is nested within more than nn quantifiers, and otherwise free.

We describe an operad LL in Set over two types, WW and PP for “words” and “propositions”, respectively. The full operad is freely generated by various disjoint suboperads

  • a free suboperad OO of operations, or functions, of types W nWW^n\to W;
  • an \mathbb{N}-indexed suboperad XX of variables of types 1W1\to W;
  • a (free) suboperad RR of predicates, or relations, of types W nPW^n\to P;
  • the equality operad, of type W 2PW^2\to P
  • the boolean operad, BB: it’s got ,,¬,\wedge, \vee,\neg,\dots of types P kPP^{k}\to P for k=1,2k=1,2, and perhaps k=0k=0 if you want to include \bot; these compose the way you think they should.
  • the quantifier :\forall:, usually written x j\forall x_j, where x jX 0x_j\in X_0; \forall is of type PPP\to P.

Notable subsets of LL include O[X]O[X], generated by OXO\cup X, the suboperad of parametrized words, and R[X]R[X], the elements of types ?P? \to P in the suboperad generated by O,R,XO,R,X.

Abusively, an LL-structure, or interpretation of the functions and relations is an algebra (W,P,O,R)(M,2,O M,R M)(W,P,O,R)\mapsto (M,2,O_M,R_M) for the suboperad QQ of LL generated by ORO\cup R with the type PP interpreted by the initial boolean algebra 22.

The Tarski Definition of Truth is a natural extension of the QQ-algebra MM to an LL-algebra, (M,)(M,\dots) such that * for Φ\Phi in R[X]R[X] and for all functions m:XMm:X\to M, the sensible thing Φ[m]\Phi[m] is true in MM. * ΦΘ\Phi \wedge \Theta is true if for all functions m:XMm:X\to M, both Φ[m]\Phi[m] and Θ[m]\Theta[m] are true, and ¬Φ\neg \Phi is true if and only if Φ\Phi is not. * (:Φ)[m](\forall:\Phi)[m] is true in MM precisely when Φ[m a]\Phi[m_a] is true for all aMa\in M, where

m a(x i)={a i=0 m(x i1) elsem_a(x_i) = \left\{ \array{ a & i=0 \\ m(x_{i-1}) & else }\right.

(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 \mathbb{N} on LL: one shifts all the variables by 1, the other adds a \forall quantifier; and the Tarski extension is the one that makes these commute somehow

ibid: maybe it’s more right to say that P MP_M should be the boolean algebra 𝒫(|M| )\mathcal{P}(|M|^\mathbb{N})? This again has that natural action of \mathbb{N} on it…

Definition and remarks

An LL-structure MM, as an LL-algebra with extra properties, defines a complete first-order theory Th(M)Th(M), that subset of LL which MM interprets as 2\top\in 2, or true. Conversely, given a collection TT of elements of LL of type ?P?\to P, we say that MTM\models T, or in words MM is a model of the theory TT whenever TTh(M)T\subset Th(M). There is an obvious Galois connection between theories TT and the collections of LL-structures that are models. Much of deeper model theory studies the fine structure of this connection.

Operads, Monads and Lawvere theories

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.

Higher-order logic

Remaining within Set, we can also generalize beyond first-order logic to various higher-order logics.

((insert your favourite variant here))

Infinitary logic and Categorical model theory

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

Important theorems

The following are closely interrelated, and depend on having a suitable universe VV. We can view them as theorems of ZFCZFC or as (relatively mild) conditions on VV.

(… clarify …)

Gödel’s completeness theorem

Given a first-order theory TT in some language LL, TT is consistent iff there is a model of TT in VV — that is, iff MTM\models T for some MVM\in V.

See at completeness theorem.

Gödel’s compactness theorem

Under the same hypotheses, TT is consistent iff every finite subset of TT is consistent; expressed semantically, a theory TT has a model iff every finite subset of TT has a model.

See at compactness theorem.

Łoś ultraproduct theorem

(…think of a good way to state this…)

See at Łoś ultraproduct theorem.

Corollaries worth thinking about

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 Th(V ω,)Th(V_\omega,\in), and any total order (X,<)(X,\lt). If one expands the language (coresponding to an injective morphism of operads) to include constant symbols c xc_x for xXx\in X, then for any subset ss of XX of finite size n+1n + 1, one has

(V ω,,0,1,,n)Th(V ω,){c xc yx<y;x,ys}(V_\omega,\in,0,1,\cdots,n)\models Th(V_\omega,\in)\cup \{c_x\in c_y \mid x\lt y;x,y\in s\}

so that the finite extensions of Th(V ω,)Th(V_\omega,\in) by suborders of XX are all consistent; by compactness, the fully extended theory Th(V ω,){c xc yx<y;x,yX}Th(V_\omega,\in)\cup \{c_x\in c_y \mid x\lt y;x,y\in X\} is also consistent; thus by completeness there is a structure (M,ϵ,,c x,)(M,\epsilon,\cdots,c_x,\cdots) such that * (M,ϵ)Th(V ω,)(M,\epsilon)\models Th(V_\omega,\in) * c xϵc yc_x\epsilon c_y for all x<yx\lt y in XX

By a similar argument, (if ZFC is consistent) there are models MM' of classical set theory satisfying the (higher-order) property that the natural numbers object ω M\omega_{M'} of MM' includes your favourite total order (X,<)(X,\lt) as a suborder — of course, MM' isn’t allowed to know this — notably, there is no object ξ\xi in MM such that {yyϵξ}={c xxX}\{y\mid y\epsilon \xi\} = \{c_x \mid x\in X\}.


Early original texts“

Discussion of classical first-order model theory includes

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)

  • Shelah archive, Shelah’s books

  • 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:

  • Valentin Goranko, Martin Otto, Model theory of modal logic, pdf

…to infinitary logic:

  • H. Keisler. Model theory for infinitary logic, North-Holland, Amsterdam, 1971.

Discussion of aspects of category theory and categorical logic (accessible categories) in model theory includes

  • Michael Makkai, Robert Paré, Accessible categories: the foundations of categorical model theory, Contemporary mathematics vol 104, AMS 1989

  • Tibor Beke, Jiří Rosický, Abstract elementary classes and accessible categories, 2011 (pdf)

  • 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

  • Anand Pillay, Geometric stability theory

  • 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

  • David Kazhdan, Lecture notes in motivic integration, with intro to logic and model theory, pdf

  • R. Cluckers, J. Nicaise, J. Sebag (Editors), Motivic Integration and its Interactions with Model Theory and Non-Archimedean Geometry, 2 vols. London Mathematical Society Lecture Note Series 383, 384

Last revised on January 23, 2023 at 11:54:28. See the history of this page for a list of all contributions to it.