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 (possibly-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, as well as the truth of predicates.