This section introduces the signatures, models, and sentences characterizing basic specifications with subsorts, extending a preceding section. The notions of satisfaction and proof system for subsorted specifications are essentially as for many-sorted specifications.
The intuition behind the treatment of subsorts adopted here is to represent subsorting by embeddings (which are not required to be identities), commuting with overloaded function symbols, as usual in order-sorted approaches. However, in the language described in the next section, instead of imposing conditions such as `regularity' on signatures, terms and sentences that can be given different parses (up to the commutativity between embeddings and overloaded symbols) are simply rejected as ill-formed.
While well-formedness of terms of the language can be checked statically, the question whether the value of a well-formed term is actually defined or not may depend on the specified axioms (and it is not decidable in general).