1.1 Signatures

A  many-sorted signature Sigma= (S,TF,PF,P) consists of:

• a set S of  sorts;
• sets TF_w,s, PF_w,s, of  total function symbols, respectively  partial function symbols, such that TF_w,s n PF_w,s = Ø, for each function  profile (w,s) consisting of a sequence of  argument sorts w  in S^* and a  result sort s  in S ( constants are treated as functions with no arguments);
• sets P_w of predicate symbols, for each predicate profile consisting of a sequence of argument sorts w  in S^*.

Note that symbols used to identify sorts, operations, and predicates may be  overloaded, occurring in more than one of the above sets. To ensure that there is no ambiguity in sentences at this level, however, function symbols f and predicate symbols p are always  qualified by profiles when used, written f_w,s and p_w respectively. (The language considered in Chapter 2 allows the omission of such qualifications when these are unambiguously determined by the context.)

A  many-sorted signature morphism sigma: (S,TF,PF,P) -> (S',TF',PF',P') consists of a mapping from S to S', and for each w  in S^*, s  in S, a mapping between the corresponding sets of function, resp. predicate symbols. A partial function symbol may be mapped also to a total function symbol, but not vice versa.