What is difference between multi-sorted model theory and single-sorted model theory?

Question

Many results about single-sorted FOL generalize to the multi-sorted setting (see here).

Are there aspects that do not generalize or are importantly different when working in a multi-sorted setting?

I am starting to work in the multi-sorted setting and am wondering if there is anything to look out for if one is used to working in the single-sorted setting.

Answer 1

In my experience, there are two main types of issues to look out for:

1. In single-sorted model theory, a structure has an unambiguous notion of cardinality (the cardinality of the underlying set). A multi-sorted structure has a family of underlying sets, one for each sort. So we can view it as having a family of cardinalities, one for each sort, or take the cardinality of the disjoint union of all the sorts. Which is more appropriate depends on the context.

2. Many results and definitions in model theory mention formulas in a single free variable. (For example, the definition of strongly minimal theory or the definition of $\kappa$-saturated model that says that every $1$-type over a set of size $<\kappa$ is realized.) In multi-sorted logic, there is no longer just one type of variable - we can think about all formulas with a single free variable from any of the sorts, or we can restrict our attention to one sort at a time. Again, which is more appropriate depends on the context.

Answer 2

I just want to add one point to Alex's answer:

In the single-sorted language, a function must have full-domain, which means that if the domain of model $\mathfrak{A}$ is $A$, then a function symbol must be interpreted as a function from $A^n$ to $A$. In contrast, multi-sorted language allows functions with partial domain. To achieve this, given several sorts $S_1,\cdots,S_n$, a function can be interpreted as a function from $S_{i_1}\times\cdots\times S_{i_m}$ to $S_j$.

A natural example is a vector space. Consider a $K$-vector space $V$. On $V$, there is an abelian group structure, as well as a well-defined action of $K$ on $V$. It is possible to add several new function symbols $\lambda_x$ for each $x\in K$, in order to define this action. However, this does not allow us to quantify over elements from $K$. However, if there are two sorts: one sort for $V$ and another for $K$, we can define the action $K\times V\to V$ uniformly.

Another example occuring in model theory a lot are imaginary sorts. Assume that $\mathfrak{A}$ is a first-order structure. Whenever there is an $\varnothing$-definable equivalence relation $E$ on $\mathfrak{A}^n$, we add a new sort $S_E$ consisting of elements corresponding to a equivalence class of $E$ with a function $\pi_E:S_{=}^n\to S_E$ sending $a$ to $a/E$. Elements in $S_E$ is called imaginary elements and $S_=$ is called the home sort, which are original elements sitting in $\mathfrak{A}$. Though it is possible to directly adding those imaginary elements to the home sort, $\pi_E$ cannot be added, because again it will become a partial function.