# In a first-order theory with multiple sorts, is there any reason not to throw away the sorts?

From a first-order theory with multiple sorts, we can obtain a theory without sorts by introducing a few predicates. For example, a vector space can be viewed as a two-sorted structure, with one sort for scalars and one for vectors. Another way of looking at it is that we can have two predicates $S(*)$ and $V(*)$ expressing the condition of a being a scalar, and of being a vector.

Is there any reason not to throw away the sorts in this way?

• You can throw away the sorts at the formal level and reintroduce them as abbreviations, Aug 20 '13 at 8:58

For example, by throwing away sorts, you will have to replace function symbols with "functional relation" symbols (i.e. relation symbols subject to suitable "function axioms"), and accordingly complicate discussion of entities like $\lambda \cdot {\bf v}$ (by writing in place of $\phi(\lambda \cdot {\bf v})$ the formula $\phi({\bf w}) \land [\cdot](\lambda, {\bf v}; {\bf w})$ where $[\cdot]$ is the relational counterpart of $\cdot$).
• Can't we just allow functions to be "under-specified"? Like, for scalars $a$ and $b$ we can require that $a \cdot b$ have the property of being a scalar, and for a scalar $a$ and a vector $\mathbf{v}$ we can require that $a \cdot \mathbf{v}$ have the property of being a vector, but if both $\mathbf{v}$ and $\mathbf{w}$ denote vectors, then we make no stipulations about $\mathbf{v} \cdot \mathbf{w}.$ Its still well-defined, but it doesn't have any useful properties. Aug 20 '13 at 10:24