nLab model theory

Idea

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

The two main problems of model theory are

• classification of a given theory $\mathcal{T}$ in a language $L$
• study the family of all definable sets of a structure $M$ of a language $L$

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

Scope

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

Examples

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

• First-order logic.

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

• Higher-order logic.

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

We describe an operad $L$ in Set over two types, $W$ and $P$ for “words” and “propositions”, respectively. The full operad is freely generated by various disjoint suboperads

• a free suboperad $O$ of operations, or functions, of types $W^n\to W$;
• an $\mathbb{N}$-indexed suboperad $X$ of variables of types $1\to W$;
• a (free) suboperad $R$ of predicates, or relations, of types $W^n\to P$;
• the equality operad, of type $W^2\to P$
• the boolean operad, $B$: it’s got $\wedge, \vee,\neg,\dots$ of types $P^{k}\to P$ for $k=1,2$, and perhaps $k=0$ if you want to include $\bot$; these compose the way you think they should.
• the quantifier $\forall:$, usually written $\forall x_j$, where $x_j\in X_0$; \forall is of type $P\to P$.

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

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

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

$$m_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 $L$: 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_M$ should be the boolean algebra $\mathcal{P}(|M|^\mathbb{N})$? This again has that natural action of $\mathbb{N}$ on it…

Definition and remarks

An $L$-structure $M$, as an $L$-algebra with extra properties, defines a complete first-order theory $Th(M)$, that subset of $L$ which $M$ interprets as $\top\in 2$, or true. Conversely, given a collection $T$ of elements of $L$ of type $?\to P$, we say that $M\models T$, or in words $M$ is a model of the theory $T$ whenever $T\subset Th(M)$. There is an obvious Galois connection between theories $T$ and the collections of $L$-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 $V$. We can view them as theorems of $ZFC$ or as (relatively mild) conditions on $V$.

(… clarify …)

Gödel’s completeness theorem

Given a first-order theory $T$ in some language $L$, $T$ is consistent iff there is a model of $T$ in $V$ — that is, iff $M\models T$ for some $M\in V$.

See at completeness theorem.

Gödel’s compactness theorem

Under the same hypotheses, $T$ is consistent iff every finite subset of $T$ is consistent; expressed semantically, a theory $T$ has a model iff every finite subset of $T$ 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_\omega,\in)$, and any total order $(X,\lt)$. If one expands the language (coresponding to an injective morphism of operads) to include constant symbols $c_x$ for $x\in X$, then for any subset $s$ of $X$ of finite size $n + 1$, one has

$$(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_\omega,\in)$ by suborders of $X$ are all consistent; by compactness, the fully extended theory $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,\epsilon,\cdots,c_x,\cdots)$ such that * $(M,\epsilon)\models Th(V_\omega,\in)$ * $c_x\epsilon c_y$ for all $x\lt y$ in $X$

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

Related entries

• model theory - contents

• definable set, definable groupoid

• type (in model theory)

• stability in model theory, geometric stability theory

• categoricity

• abstract model theory

• generalized quantifier

• nonstandard analysis, set theory, foundations and logic, algebraic set theory, forcing, o-minimal structure

• Lascar group

• Birkhoff's HSP theorem

• model theory and physics

• entries on researchers in model theory: Alfred Tarski, Boris Zilber, Kenneth Kunen, Saharon Shelah

References

Early original texts“

• Simon Kochen, p. 223 in: Ultraproducts in the Theory of Models, Ann. Math. 74 2 (1961) 221-261 [doi:10.2307/1970235]

  (also introducing the notation for “$\vDash$-judgements”, cf. there)

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)

• 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