Models

For a many-sorted signature Sigma= (S,TF,PF,P) a  many-sorted model M e Mod(Sigma) is a  many-sorted first-order structure consisting of a  many-sorted partial algebra:

• a non-empty  carrier set s^M for each sort s e S (let w^M denote the Cartesian product s₁^M×···×s_n^M when w=s₁...s_n),
• a  partial  function f^M from w^M to s^M for each function symbol f e TF_w,s or f e PF_w,s, the function being required to be total in the former case,

• a  predicate p^M C w^M for each predicate symbol p e P_w.

A (weak)  many-sorted homomorphism h from M₁ to M₂, with M₁, M₂ e Mod(S,TF,PF,P), consists of a function h_s:s^M₁ -> s^M₂ for each s e S preserving not only the values of functions but also their definedness, and preserving the truth of predicates.

Any signature morphism sigma:Sigma -> Sigma' determines the  many-sorted reduct of each model M' e Mod(Sigma') to a model M e Mod(Sigma), defined by interpreting symbols of Sigma in M in the same way that their images under sigma are interpreted in M'.