This topic is not about definitions, but something not far from, as we may think that sorts are definable somehow in logic without sorts. The topic itself arose in our google group as follows:

"[Alex:]> It's like with many-sorted logics: any set of sorts may be reduced to set of unary predicates with disjoint axiom. As Maltzev mentioned in his book "Algebraic systems".

[JFS:]Yes, but. And this is a very big **BUT**: The set of models of the axioms with the reduced version is much, much bigger than the set of models of the sorted logic. This is significant for theorem proving. The proofs with sorted logic can be orders of magnitude faster than the proofs with the reduced version.

There are also important proofs about sorted logic that are not true about the reduced version. For quotations and citations, see http://jfsowa.com/logic/sorts.pdf " Template:Wl-publish: 2018-04-23 10:49:59 -0400