Given a first-order language , which consists of symbols (variable symbols, constant symbols, function symbols and relation symbols including ) and quantifiers; a structure for , or -structure is a set with an interpretation for symbols:
if is an -ary relation symbol, then its interpretation
if is an -ary function symbol, then is a function
if is a constant symbol, then
The underlying set of the structure is referred to as (universal) domain of the structure (or the universe of the structure).
Interpretation for an -structure inductively defines an interpretation for well-formed formulas in . We say that a sentence is true in if is true. Given a theory , which is a language together with a given set of sentences in , the interpretation in a structure makes those sentences true or false; if all the sentences in are true in we say that is a model of .
In model theory, given a language , a structure for is the same as a model of 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.
Every first-order language gives rise to a first-order hyperdoctrine with equality freely generated from . Denoting this by , the base category 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 depends to some extent on the logic we wish to impose; for example, we could take the free Boolean hyperdoctrine generated from if we work in classical logic.
There is also a “tautological” first order hyperdoctrine whose base category is , and whose predicates are given by the power set functor
and then an interpretation of , as described above, amounts to a morphism of hyperdoctrines .
This observation opens the door to a widened interpretation of “interpretation”, where we might for instance replace Set by a topos , and use instead (taking an object of to its Heyting algebra of subobjects) as the receiver of interpretations. This of course is just one of many possibilities.