Functions in many-sorted logic

176 Views Asked by At

It seems that one can turn a family of multi-sorted structures:

$\mathcal{M} = \langle \langle M_j \rangle_{j \in J}; \ldots \rangle$

into a single-sorted structure:

$\mathcal{M}_U = \langle \cup_{j \in J} M_j; \langle M_j \rangle_{j \in J}, \ldots \rangle$

But what happens with functions? Suppose I have a function:

$f: M_1 \times M_2 \to M_2$

How do I represent it in the single-sorted structure?

References

Feferman, 1974

2

There are 2 best solutions below

2
On BEST ANSWER

More precisely, one turns $\mathcal{M} = \{M_j\}_{j \in J}$ into the set $\coprod\limits_{j \in J} M_j$ (since we don't necessarily know that the $M_j$ are pairwise disjoint).

Hopefully, it's clear that we can take a relation $P \subseteq M_{j_1} \times M_{j_2} \times ... \times M_{j_n}$ and turn it into $P_U \subseteq \mathcal{M}_U^n$ in the obvious way.

For functions, there isn't a nice, natural way to turn a function $M_i \to M_j$ into a function $\mathcal{M}_U \to \mathcal{M}_U$.

However, we can express the function $f$ as a relation $f \subseteq M_1 \times M_2$ and then turn the relation into a relation $f_U \subseteq \mathcal{M}_U^2$.

For your example, we would take a function $f : M_1 \times M_2 \to M_2$, express it as a relation $f \subseteq M_1 \times M_2 \times M_2$, and then construct $f_U \subseteq \mathcal{M}_U^3$.

0
On

Mark has already completely resolved your question (+1), but let me discuss a bit the following more general question: to what degree can we approximate many-sorted logic within one-sorted logic? If $T_m$ is a theory in a family $(S_j)_{j\in J}$ of sorts, then one might try the following naive approach for converting $T_m$ into a one-sorted theory $T_1$: add $1$-ary predicate symbols $(P_j)_{j\in J}$ to the language for each sort, replace the function symbols of $T_m$ with corresponding predicate symbols as indicated in Mark's answer, and then form $T_1$ by (i) adding axioms saying that the $P_i$ are all pairwise disjoint, and (ii) "relativizing" all of the many-sorted axioms of $T_m$ to the relevant predicate symbols of $T_1$.

This seems at first glance to provide a satisfactory approximation of many-sorted logic, but unfortunately it can start to fall short in critical ways if $J$ is infinite. For instance, contrast the following two situations. Consider first a many-sorted theory $T_m$, with sorts $(S_i)_{i\in\omega}$, in the empty language. Let $T_m$ have axioms expressing that each $S_i$ has infinitely many elements; then $T_m$ is complete (and indeed, is $\aleph_0$-categorical).

Now, if we were to carry out the process we've outlined above for $T_m$, we'd wind up with a theory $T_1$, in the language $L_1=(P_i)_{i\in\omega}$, whose axioms state that (i) the realizations of the $P_i$ are pairwise disjoint, and that (ii) each $P_i$ has infinitely many realizations. This theory is again complete, and certainly any model of $T_m$ can be realized in a natural way as a model of $T_1$: given a model $M=(M_i)_{i\in\omega}\models T_m$, the structure $\bigsqcup_{i\in\omega}M_i$ becomes a model of $T_1$ by realizing each $P_i$ as the corresponding copy of $M_i$. But we cannot go in the other direction; for example, the set $N=\omega\times\omega\sqcup\{\star\}$ becomes a model of $T_1$ by realizing each $P_i$ as the subset $\{i\}\times\omega\subset N$. But there is no natural way to convert this into a model of $T_m$: indeed, in $N$, we have an element $\star$ that does not belong to any $P_i$! So, if the $P_i$ are supposed to be one-sorted "approximations" of the sorts of $T_m$ in $T_1$, then the model $N\models T_1$ has an element that does not belong to any "sort", which is incompatible with the definitions of many-sorted logic.

Since $T_1$ is complete, there's no way to resolve this problem merely by adding more axioms; many-sorted logic has properties that simply cannot be naively approximated by just adjoining new predicate symbols to a one-sorted language. The fundamental problem is that the compactness theorem applies to predicate symbols, but not to sorts; if we have infinitely many non-empty, pairwise disjoint predicate symbols, then the partial type that says "I do not belong to any of these predicate symbols" is necessarily consistent with the ambient theory. So, in some elementary extension, we can always find elements outside a given family of such predicates. There is nothing analogous with sorts, which makes sorts, in a precise sense, much more rigid than predicates of first-order logic can be.

Thus, depending on what you're looking for in an "approximation" of many-sorted logic by one-sorted logic, the naive approach fails. It was a postulate of Quine's – in an informal sense – that every many-sorted theory should be equivalent in some suitable sense to a one-sorted theory. Some discussion on this question can be found in this paper, which tries to formulate and prove an appropriate form of this idea.