3

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?

goblin GONE
  • 67,744

2 Answers2

7

You can throw away sorts, in the way you describe. Of course, quantification, functions, and relations (and practically all formulae) become (much) more tedious to express by doing this.

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$).

In short, it adds to conceptual clarity and readability to have sorts. But the expressivity of the language does not increase by using them, as you correctly point out.

Lord_Farin
  • 17,743
  • 1
    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. – goblin GONE Aug 20 '13 at 10:24
  • 1
    @user18921 That's possible, but it gives rise to problems when proving two structures are elementarily equivalent, because these "underspecified parts" of the function still need an interpretation in every structure; this interpretation will make certain, more or less random sentences true in the structure, that we are not interested in. On a deeper level, you could of course change the notion of "structure" to allow function symbols to be interpreted by partial functions; I have no idea where this line of thought may lead to (but it is reminiscent of computability theory). – Lord_Farin Aug 20 '13 at 10:43
6

As you note, technically there's a standard but artificial trick for regimenting the natural many-sorted language of mathematicians into a single sorted formal language. Now, there's always a trade-off in regimentations between sticking more closely to the logical shape of the discourse we are regimenting and getting a slicker formal calculus which is easier to theorize about. And in this case, for many purposes, the price is right -- a certain cost in readability buys us a formalism that appeals to logicians' appetite for clean Bauhaus lines.

But, some would say, we shouldn't let the availability of the trick lead us astray. Some working mathematicians (round my neck of the woods) take their mathematical universes to be strongly typed -- real numbers (say) are one sort of thing, vectors (say) are another sort of thing, and sets (say) are yet another sort of thing. You can model or represent numbers and vectors as sets, but it's a kind of pointless philosophical nonsense (they'd say) to ask whether numbers really are sets, for example. The numbers and the sets belong to different mathematical universes. Conceptually speaking, these mathematicians might say, the trouble about regimenting talk about reals and vectors and sets as talk of objects belonging to One Big Domain is that it encourages some nonsense questions about which objects in the domain are identical to other objects alongside the sensible questions. So, conceptually, it is better to stick with the everyday mathematicians' sorted talk. Or so the story goes. (I'm not endorsing it, just gesturing to why it might be wondered whether the technical trick is merely technical.)

Peter Smith
  • 54,743