**Go backward to** 1.1 Signatures

**Go up to** 1 Basic Concepts

**Go forward to** 1.3 Sentences

## 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 non-empty
*carrier set* *s*^{M} for each sort *s ***e*** S* (let
*w*^{M} denote the Cartesian product *s*_{1}^{M}×···×s_{n}^{M}
when *w=s*_{1}...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,

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*_{1} to *M*_{2},
with *M*_{1}, M_{2} **e*** * **Mod***(S,**TF*,*PF*,P), consists of a function
*h*_{s}:s^{M1} -> s^{M2} 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'*.

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk