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 sM for each sort s e S (let wM denote the Cartesian product s1M×···×snM when w=s1...sn),
• a  partial  function fM from wM to sM for each function symbol f e TFw,s or f e PFw,s, the function being required to be total in the former case,
together with:
• a  predicate pM c wM for each predicate symbol p e Pw.

A (weak)  many-sorted homomorphism h from M1 to M2, with M1, M2 e Mod(S,TF,PF,P), consists of a function hs:sM1 -> sM2 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.