8.2 Term models
Let \( L \) be a \( \Sigma \)-language. A 1-\( L \)-formula of sort \( A \) is an \( L \)-bounded formula on \( \operatorname {\mathsf{Empty}} \) with one additional free variable of sort \( f : \operatorname {\mathsf{Fin}}1 \to \Sigma \) given by \( f(x) = A \).
Let \( L \) be a \( \Sigma \)-language. The witness symbols for \( L \) is the language \( L_W \) consisting of a single constant of sort \( A \) for every 1-\( L \)-formula of sort \( A \).
Let \( M \) be a nonempty \( L \)-structure. Then \( M \) has an \( L_W \)-structure such that for each 1-\( L \)-formula \( \phi \) of sort \( A \), there is a constant symbol \( c : \operatorname {\mathsf{Functions}}(0, \# [], A) \) such that
We define the interpretation of the constant for \( \phi \) to be some \( x : M \) such that \( M \vDash \phi (x) \) if one exists, or an arbitrary \( y : M \) otherwise. 1 This defines an \( L_W \)-structure for \( M \), and clearly \( M \) satisfies the required property.
For each \( n : \mathbb N \), we define
This forms a directed diagram of languages, which has a colimit \( L^{(\omega )} \). There are natural morphisms \( L \to L^{(\omega )} \) and \( L^{(n)} \to L^{(\omega )} \) which are expansions on \( M \).
Let \( M \) be a nonempty \( L \)-structure. Then \( M \) has an \( L^{(\omega )} \)-structure such that for each 1-\( L^{(\omega )} \)-formula \( \phi \) of sort \( A \), there is a constant symbol \( c : \operatorname {\mathsf{Functions}}(0, \# [], A) \) such that
Then, by the Tarski–Vaught test (which must be proven in the many-sorted case), the set \( N \subseteq M \) comprised of all of the interpretations of \( L^{(\omega )} \)-terms, is the domain of an \( L^{(\omega )} \)-elementary substructure of \( M \).
This will take substantial work.