A many-sorted signature Sigma= (S,TF,PF,P) consists of:
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 fw,s and pw 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 e S*, s e 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.