1.2 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),

  [AT] So, we are back to models with possibly empty carriers. I don't recall the explicit argument for going back to this, but I do recall that this didn't fit nicely together with the role of variable declarations and their use in the interpretation of axiom declarations. If I understand what is there now, we surround each axiom with universal quantification over all variables declared (see a later section). This was one of the combinations rejected in Edinburgh, I thought. Of course one can live with this, since after all one can simply never declare any variables and use only explicit quantification.

  Discharged: Empty carriers are disallowed.

• 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,

together with:

• 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.

[AT] Reducts of models w.r.t. signature morphisms should be mentioned, since they are used in further explanations.

Discharged: Adjust text accordingly.

---

CoFI Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk