nLab model


This page is about the notion of model in logic. For the notion in physics see model (in theoretical physics).



In model theory, a model of a theory is a realization of the types, operations, relations, and axioms of that theory. In ordinary model theory one usually studies mainly models in sets, but in categorical logic we study models in other categories, especially in topoi.

The term structure is often used to mean a realization of types, operations, and relations in some signature, but not satisfying any particular axioms. This is of course the same as a model for the “empty theory” in that signature, which has the same types, operations, and relations, but no axioms at all. One then talks about whether a given structure is, or is not, a model of a given theory in a given signature.


In first-order theories

The basic concept is of a structure for a first-order language LL: a set MM together with an interpretation of LL in MM. A theory TT is specified by a language and a set of sentences in LL.

An LL-structure MM is a model of TT if for every sentence ϕ\phi in TT, its interpretation in MM, ϕ M\phi^M is true (“ϕ\phi holds in MM”).

We say that TT is consistent or satisfiable (relative to the universe in which we do model theory) if there exist at least one model for TT (in our universe). Two theories, T 1T_1, T 2T_2 are said to be equivalent if they have the same models.

Given a class KK of structures for LL, there is a theory Th(K)Th(K) consisting of all sentences in LL which hold in every structure from KK. Two structures MM and NN are elementary equivalent (sometimes written by equality M=NM=N, sometimes said “elementarily equivalent”) if Th(M)=Th(N)Th(M)=Th(N), i.e. if they satisfy the same sentences in LL. Any set of sentences which is equivalent to Th(K)Th(K) is called a set of axioms of KK. A theory is said to be finitely axiomatizable if there exist a finite set of axioms for KK.

A theory is said to be complete if it is equivalent to Th(M)Th(M) for some structure MM.

For Lawvere theories

For Syn(T)Syn(T) the syntactic category of an algebraic theory (where Syn(T)Syn(T) is perhaps better known as a Lawvere theory), and for CC any category with finite limits, a model for TT in CC is a product-preserving functor

N:Syn(T)C. N : Syn(T) \to C \,.

The category of models in this case is hence the full subcategory of the functor category [Syn(T),C][Syn(T),C] on product-preserving functors.


Last revised on February 16, 2015 at 20:13:23. See the history of this page for a list of all contributions to it.