A subsorted signature Sigma=(S,TF,PF,P, < S) consists of a many-sorted signature (S,TF,PF,P) together with a pre-order < S of subsort embeddings on the set S of sorts. < S is extended to sequences of sorts.
[DTS] How is it extended? (Pointwise: s1...sn < s'1...s'n iff sj < s'j for all 1 < j < n)
Discharged: Adjust wording.We may drop the subscript S when obvious from the context.
For a subsorted signature, we can define overloading relations for function and predicate symbols. Let f1:w1 -> s1 < F f2:w2 -> s2 hold if w1 < w2, s1 and s2 have a common supersort, and f1=f2; similarly for predicate symbols, let p1:w1 < P p2:w2 hold if w1 < w2 and p1=p2.
A subsorted signature morphism sigma: Sigma -> Sigma' is a many-sorted signature morphism that preserves the pre-order < S and the overloading relations < F and < P.
With each subsorted signature Sigma=(S,TF,PF,P, < S) a many-sorted signature Sigma# is associated, extending (S,TF,PF,P) for each pair of sorts s < S s' by a total embedding function (from s into s'), a partial projection function (from s' onto s), and a membership predicate (testing whether values in s' are embeddings of values in s). We assume that the symbols used for embeddings, projections and membership are not used otherwise in Sigma.
[DTS] I think the point is that they are chosen arbitrarily so as not to be used otherwise in Sigma -- they will never be referred to by name so their names don't matter.
Discharged: Adjust wording if convenient.
[AT] I think we need a remark here that any subsorted signature morphism sigma: Sigma1 -> Sigma2 expands to a signature morphism sigma# : Sigma1# -> Sigma2# in the obvious way (preserving projection, embedding and membership symbols). Then in the next subsection we may just remark that the reduct of a model w.r.t. a subsorted signature morphism sigma is its usual reduct w.r.t. sigma#.
Discharged: Adjust wording.