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.

A model theory for a particular logic typically works within a given universe, and specifies a notion of 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 $L$ via a given set $M$ together with interpretation of the symbols of the language. A model of a theory $𝒯$ in the language $L$ is an L-structure which satisfies each formula in $𝒯$.

The two main problems of model theory are

• classification of a given theory $𝒯$ 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, and the subcollection of those structures verifying a given collection $\mathrm{Th}$ of propositions in the language are an interesting subcategory again.

Examples

First-order logic

See also/first 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 $\perp$; 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)=\{\begin{array}{cc}a& i=0\\ m(x_{i-1})& \mathrm{else}\end{array}$$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 $𝒫(\mid M{\mid }^{\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 $\mathrm{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\vDash T$, or in words $M$ is a model of the theory $T$ whenever $T\subset \mathrm{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 and Algebras

Focusing on the obvious words “operad” and “algebra”, it’s popular in local quarters to simply understand “operad” for “theory”, and “algebra” for model. See operad for more.

(…)

Lawvere Theories

Lawvere theory

(…)

Higher-order logic

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

((insert your favourite variant here))

Important results

The following are closely interrelated, and depend on having a suitable universe $V$. We can view them as theorems of $\mathrm{ZFC}$ or as (relatively mild) conditions on $V$.

(… clarify …)

Goedel 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\vDash T$ for some $M\in V$.

Goedel’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.

Łoś ultraproduct theorem

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

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 $\mathrm{Th}(V_{\omega },\in )$, and any total order $(X,<)$. 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)\vDash \mathrm{Th}(V_{\omega },\in )\cup \{c_x\in c_y\mid x<y;x,y\in s\}$$(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 $\mathrm{Th}(V_{\omega },\in )$ by suborders of $X$ are all consistent; by compactness, the fully extended theory $\mathrm{Th}(V_{\omega },\in )\cup \{c_x\in c_y\mid x<y;x,y\in X\}$ is also consistent; thus by completeness there is a structure $(M,ϵ,\cdots ,c_x,\cdots )$ such that

• $(M,ϵ)\vDash \mathrm{Th}(V_{\omega },\in )$
• $c_xϵc_y$ for all $x<y$ in $X$

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

Related entries

• definable set, definable groupoid

• type (in model theory)

• stability in model theory, geometric stability theory

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

• Lascar group

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

Literature

• Chen Chung Chang, H. Jerome Keisler, Model Theory. Studies in Logic and the Foundations of Mathematics. 1973, 1990, Elsevier.

• Wilfrid Hodges, Model Theory, Cambridge University Press 1993; A shorter model theory, Cambridge UP 1997

• 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

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

• 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

• Shelah archive, Shelah’s books

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

• John T. Baldwin, Fundamentals of stability theory

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

• Gerald E Sacks, Saturated model theory, Benjamin 1972

• wikipedia model theory