nLab
structure in model theory

Idea

Given a first-order language $L$, which consists of symbols (variable symbols, constant symbols, function symbols and relation symbols including $ϵ$) and quantifiers; a structure for $L$, or $L$-structure is a set $M$ with an interpretation for symbols:

• if $R\in L$ is an $n$-ary relation symbol, then its interpretation $R^M\subset M^n$

• if $f\in L$ is an $n$-ary function symbol, then $f^M:M^n\to M$ is a function

• if $c\in L$ is a constant symbol, then $c^M\in M$

The underlying set $M$ of the structure is referred to as (universal) domain of the structure (or the universe of the structure).

Interpretation for an $L$-structure inductively defines an interpretation for well-formed formulas in $L$. We say that a sentence $\varphi \in L$ is true in $M$ if ${\varphi }^M$ is true. Given a theory $(L,T)$, which is a language $L$ together with a given set $T$ of sentences in $L$, the interpretation in a structure $M$ makes those sentences true or false; if all the sentences in $T$ are true in $M$ we say that $M$ is a model of $(L,T)$.

In model theory, given a language $L$, a structure for $L$ is the same as a model of $L$ as a theory with an empty set of axioms. Conversely, a model of a theory is a structure of its underlying language that satisfies the axioms demanded by that theory.

There is a generalization of structure for languages/theories with multiple domains or sorts, called multi-sorted languages/theories.

Categorical interpretation

Every first-order language $L$ gives rise to a first-order hyperdoctrine with equality freely generated from $L$. Denoting this by $T(L)$, the base category $C_{T(L)}$ consists of sorts (which are products of basic sorts) and functional terms between sorts; the predicates are equivalence classes of relations definable in the language. The construction of $T(L)$ depends to some extent on the logic we wish to impose; for example, we could take the free Boolean hyperdoctrine generated from $L$ if we work in classical logic.

There is also a “tautological” first order hyperdoctrine whose base category is $\mathrm{Set}$, and whose predicates are given by the power set functor

$$P:{\mathrm{Set}}^{\mathrm{op}}\to \mathrm{Bool}$$P \colon Set^{op} \to Bool

and then an interpretation of $L$, as described above, amounts to a morphism of hyperdoctrines $T(L)\to \mathrm{Taut}(\mathrm{Set})$.

This observation opens the door to a widened interpretation of “interpretation”, where we might for instance replace Set by a topos $E$, and use instead $\mathrm{Sub}:E^{\mathrm{op}}\to \mathrm{Heyt}$ (taking an object of $E$ to its Heyting algebra of subobjects) as the receiver of interpretations. This of course is just one of many possibilities.