its type language when all tuples are classified by that expression. In
other words, a model satisfies an expression when that expression holds
for all tuples; i.e., has maximal extent in the expression
classification. A model for a theory is a model that satisfies every
axiom of that theory. Every model generates a theory, whose base
language is the underlying type language of the model, and whose axioms
are all expressions satisfied by the model. The theory of a model is
closed, and is the maximal theory 