# How to interpret functional symbols in a many-sorted language in the corresponding single-sorted language?

I was reading about Many-sorted logic and I kept seeing a lot of authors claiming that "When there are only finitely many sorts in a theory, many-sorted first-order logic can be reduced to single-sorted first-order logic".

I get that this is done by introducing, for every sort $$a$$, a unary predicate symbol $$P_a$$ and by adding axioms saying that these unary predicates partition the domain, but I don't get how this works for functions. Let me give you an example:

We can talk about vector spaces over a field $$\mathbb F$$ using a many-sorted language with two sorts: $$F$$ (for scalars of the field) and $$V$$ (for vectors). To talk about scalar multiplication, we would introduce a binary function symbol $$\langle\cdot,\cdot\rangle$$ with sort type $$(F,V,V)$$ which in the many-sorted structure will be interpreted as a function $$\langle\cdot,\cdot\rangle:\mathbb{F}\times V \to V$$.

However, when we translate this into single-sorted FOL, our structure, even if it has predicates $$P_F$$ and $$P_V$$ will only have one universe $$U$$, and thus the interpretation of $$\langle\cdot,\cdot\rangle$$ will have to be a function $$\langle\cdot,\cdot\rangle:U\times U\to U$$

and this means that we will have to define what $$\langle v,w \rangle$$ is where both $$v,w$$ happen to be vectors.

How can this be overcome when translating many-sorted logic to single-sorted logic when there are only a finite number of sorts?

• We have to make sure that all the axioms about $\langle x,y\rangle$ include the hypotheses $P_F(x)$ and $P_V(y)$ in the right places so that it doesn't matter how we interpret $\langle x,y\rangle$ when $x,y$ have the wrong types. This can be done in a systematic way.
– Karl
Feb 27 at 23:41
• The tag many-sorted-logic does not already exist on this site. In general, we ask that users not create new tags without first running new tag ideas by the community. math.meta.stackexchange.com/q/35451 Mar 1 at 12:04

Rob Arthan's answer is correct, but it has the downside that if $$T$$ is a many-sorted theory and $$T'$$ is the corresponding single-sorted theory, then $$T$$ and $$T'$$ fail to be bi-interpretable (since the "junk" interpretations of the functions symbols outside of their intended domains cannot be recovered after passing from a model of $$T'$$ to a model of $$T$$).
An alternative is simply to replace every function symbol with a relation symbol defining its graph. So for example replace scalar multiplication with a ternary relation symbol $$R$$ and add the axioms $$\forall x\forall y\forall z\,(R(x,y,z)\to P_F(x)\land P_V(y)\land P_V(z))$$ and $$\forall x\forall y\,(P_F(x)\land P_V(y)\to \exists^! z\, R(x,y,z)).$$ Following this approach, we can find a single-sorted $$T'$$ which is actually bi-interpretable with $$T$$.
When you reduce a many-sorted language to a single-sorted language, you relativise all the axioms using predicates representing the sorts. So, for example, if $$F$$ and $$V$$ denote the sorts for the field elements and the vectors in a theory of vector spaces, the axiom $$\forall x^F, v^V, w^V \cdot x(v + w) = xv + xw$$ translates into $$\forall x, v, w\cdot P_F(x) \land P_V(v) \land P_V(w) \Rightarrow x(v + w) = xv + xw$$ The function symbols for scalar-vector multiplication and vector-vector addition are functions $$U \times U \to U$$, so that ill-typed terms like $$x + v$$ (where $$x$$ is a scalar and $$v$$ is a vector) are syntactically allowed. The relativisation means that the translated axioms say nothing about the meaning of these ill-typed terms.