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

Question

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?

Answer 1

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

Answer 2

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.

If all you are after is a reduction of predicates in the many-sorted language to equiprovable sentences in the single-sorted language, you don't need to add axioms saying that the sort predicates partition the domain. If you follow the usual convention that sorts are non-empty, you do need axioms to say that each sort predicate is satisfiable.