A \( \Sigma \)-language consists of a map \( \operatorname {\mathsf{Functions}} : \prod _{n : \mathbb N} (\operatorname {\mathsf{Fin}}n \to \Sigma ) \to \Sigma \to \mathsf{Type}_u \) and a map \( \operatorname {\mathsf{Relations}} : \prod _{n : \mathbb N} (\operatorname {\mathsf{Fin}}n \to \Sigma ) \to \mathsf{Type}_v \).

Let \( \Phi : \Sigma \to \Sigma ' \). Let \( L \) be a \( \Sigma \)-language and let \( L' \) be a \( \Sigma ' \)-language. Then a \( \Phi \)-morphism of languages \( L \xrightarrow \Phi L' \) consists of a map

and a map

If \( L, L' \) are \( \Sigma \)-languages, we may simply say that a morphism of languages \( L \to L' \) is a \( \operatorname {\mathsf{id}}_\Sigma \)-morphism \( L \xrightarrow {\operatorname {\mathsf{id}}_\Sigma } L' \). ¹

Let \( L, L' \) be \( \Sigma \)-languages. We define \( L \oplus L' \) to be the \( \Sigma \)-language with

and

There are morphisms of languages \( L, L' \to L \oplus L' \).

Let \( L \) be a \( \Sigma \)-language, and let \( M : \Sigma \to \mathsf{Type}_w \). An \( L \)-structure on \( M \) consists of a map

and a map

We will write \( f^M \) for \( \operatorname {\mathsf{funMap}}(n, A, B, f) \), and similarly \( R^M \) for \( \operatorname {\mathsf{relMap}}(n, R) \). If \( M \) is an \( L \)-structure and an \( L' \)-structure, it is also naturally an \( (L \oplus L') \)-structure. If \( M \) is an \( L \)-structure and an \( L' \)-structure, then a morphism of \( \Sigma \)-languages \( \Phi : L \to L' \) is called an expansion on \( M \) if it commutes with the interpretations of all symbols on \( M \).

Let \( L \) be a \( \Sigma \)-language. A morphism of \( L \)-structures \( M \to N \) consists of functions \( h_A : M_A \to N_A \) such that for all \( n : \mathbb N \), \( A : \operatorname {\mathsf{Fin}}n \to \Sigma \), and \( B : \Sigma \), all function symbols \( f : \operatorname {\mathsf{Functions}}(n, A, B) \), and all \( x : \prod _{i : \operatorname {\mathsf{Fin}}n} M(A(i)) \),

and for all relation symbols \( R : \operatorname {\mathsf{Relations}}(n, A) \),

Let \( L \) be a \( \Sigma \)-language, and let \( \alpha : \mathsf{Type}_{u'} \) be a sort of variables of sort \( S : \alpha \to \Sigma \). An \( L \)-term on \( \alpha : S \) of sort \( A \), the type of which is denoted \( \operatorname {\mathsf{Term}}_{\alpha :S} A \), is either

• a variable, comprised solely of a name \( n : \alpha \) such that \( S(n) = A \), or

• an application of a function symbol, comprised of some \( n : \mathbb N \), a map \( B : \operatorname {\mathsf{Fin}}n \to \Sigma \), a function symbol \( f : \operatorname {\mathsf{Functions}}(n, B, A) \), and terms \( t : \prod _{i : \operatorname {\mathsf{Fin}}n} \operatorname {\mathsf{Term}}_{\alpha :S} B(i) \).

Let \( L \) be a \( \Sigma \)-language, and let \( \alpha : \mathsf{Type}_{u'} \) and \( S : \alpha \to \Sigma \). We define the type of \( L \)-bounded formulae on \( \alpha : S \) with free variables indexed by \( \alpha \), and \( n \) additional free variables of sorts \( f : \operatorname {\mathsf{Fin}}n \to \Sigma \), denoted \( \mathsf{BForm}_{\alpha :S}^f \), by the following constructors.

• \( \operatorname {\mathsf{falsum}} : \mathsf{BForm}_{\alpha :S}^f \);

• \( \operatorname {\mathsf{equal}} : \prod _{A : \Sigma } \operatorname {\mathsf{Term}}_{\alpha \oplus \operatorname {\mathsf{Fin}}n : S \oplus f} A \to \operatorname {\mathsf{Term}}_{\alpha \oplus \operatorname {\mathsf{Fin}}n : S \oplus f} A \to \mathsf{BForm}_{\alpha :S}^f \);

• \( \operatorname {\mathsf{rel}} : \prod _{m : \mathbb N} \prod _{B : \operatorname {\mathsf{Fin}}m \to \Sigma } \prod _{R : \operatorname {\mathsf{Relations}}(m, B)} \left( \prod _{i : \operatorname {\mathsf{Fin}}m} \operatorname {\mathsf{Term}}_{\alpha \oplus \operatorname {\mathsf{Fin}}n : S \oplus f} B(i) \right) \to \mathsf{BForm}_{\alpha :S}^f \);

• \( \operatorname {\mathsf{imp}} : \mathsf{BForm}_{\alpha :S}^f \to \mathsf{BForm}_{\alpha :S}^f \to \mathsf{BForm}_{\alpha :S}^f \); and

• \( \operatorname {\mathsf{all}} : \prod _{A : \Sigma } \mathsf{BForm}_{\alpha :S}^{A :: f} \to \mathsf{BForm}_{\alpha :S}^f \),

where the syntax \( A :: f \) denotes the cons operation on maps from \( \operatorname {\mathsf{Fin}}n \). ² An \( L \)-formula on \( \alpha : S \) with free variables indexed by \( \alpha \) is an inhabitant of \( \mathsf{BForm}_{\alpha :S}^{\# []} \). ³ An \( L \)-sentence is an \( L \)-formula with free variables indexed by \( \operatorname {\mathsf{Empty}} : f \), where \( f \) is the unique function \( \operatorname {\mathsf{Empty}} \to \Sigma \). An \( L \)-theory is a set of \( L \)-sentences.