4.2 A generalised subsorted logic

A generalised subsorted signature Sigma= (S, TF, PF, P, < ¹, < ²) consists of a many-sorted signature (S, TF, PF, P) together with two pre-orders < ¹ and < ² of subsort embeddings on the set S of sorts, for which < ¹ is a suborder of < ².

The associated many-sorted signature Sigma^# is now the extension of (S,TF,PF,P) with

1. a total embedding function symbol (from s to s') for each pair of sorts s < ² s'
2. a partial projection function symbol (from s' to s) for each pair of sorts s < ¹ s'
3. and a unary membership predicate symbol (testing whether terms of sort s' are embeddings of values in s) for each pair of sorts s < ² s'

Sigma sentences are many-sorted Sigma^# sentences.

Sigma models are many-sorted Sigma^# models satisfying a collection of axioms ensuring that embeddings inj: s -> s' are injective for s < ¹ s', ...

Note that the axiom defining the meaning of membership must now be stated in terms of embedding functions instead of projection functions.