I know that unsorted FOL is equivalently expressive to finitely-many-sorted FOL. The only semantic criteria placed on the sorts in the many-sorted FOL are that every object in the domain is in one of the sorts, and the sorts are disjoint subsets of the domain. All the statements in unsorted FOL can be trivially mapped to statements in just one of the sorts of the many-sorted logic, in both the finite & infinite case, and both should have all the same models.
To translate from N-sorted FOL to unsorted FOL, we can add unary relation symbols $S_1, ..., S_N$ and then we add axioms that state that they are disjoint and cover the whole set:
$\forall x, S_1(x) \vee ... \vee S_N(x)$
and for every pair of sort-symbols $S, S'$, the axiom:
$\neg(\exists x, S(x) \wedge S'(x))$
For every constant symbol c meant to be interpreted as being in sort S, we add the axiom:
$S(c)$
Then anywhere you do a quantification over a sort S in N-sorted logic like
$\forall x : S, P(x)$
we can translate this to an equivalent unsorted FOL statement in our new theory:
$\forall x, S(x) \implies P(x)$
To attempt to translate from infinitely-many-sorted FOL to unsorted FOL, we can add unary relation symbols $S_1, S_2,...$ for each sort, and then add the axioms
$\forall x, \phi(x)$
and for every pair of sort-symbols $S, S'$, the axiom
$\neg(\exists x, S(x) \wedge S'(x))$
and for every constant symbol c meant to be interpreted as being in sort S, the axiom:
$S(c)$
Where $\phi(x)$ stands for an FOL formula expressing that the object $x$ is in at least one of the sorts. We'll call this theory $T$. The formula $\phi(x)$ must be semantically equivalent to the following infinite disjunction of statements:
$S_1(x) \vee S_2(x) \vee ...$
The negation of $\forall x, \phi(x)$ must therefore be equivalent to the statement:
$\exists x, \neg S_1(x) \wedge \neg S_2(x) \wedge ...$
Skolemizing, we can add a fresh constant symbol $\sigma$ and create an equisatisfiable formula:
$\neg S_1(\sigma) \wedge \neg S_2(\sigma) \wedge ... $
This is an infinite conjunction of finite first-order statements, and thus represents a first-order theory, call it $\neg T$. Because we assumed $T$ was a first-order theory, then $T \cup \neg T$ is also a first-order theory.
$T \cup \neg T$ is not satisfiable, because $\neg T$ semantically contradicts $\forall x, \phi(x)$, in the case where $x = \sigma$. By the compactness theorem, there must exist some finite subset of $T \cup \neg T$ which is not satisfiable.
However, it's straightforward to see that every finite subset is satisfiable: choose a structure where the objects are the constant symbols $c$ such that the axiom $S(c)$ is included in your subset, for some sort symbol $S$, and map every sort symbol $S$ to the unary relation that holds for an object $c$ iff the axiom $S(c)$ is included in your subset; choose your structure such that for the interpretations of any two sort symbols $S, S'$ are disjoint sets of the domain; if for every axiom $S(c)$ included in your subset, the axiom $\neg S(\sigma)$ is also included in your subset, then choose another sort symbol $S'$ such that the axiom $\neg S'(\sigma)$ is not included in your subset, add a new object in the domain to represent $\sigma$ and map $S'$ to a unary relation on the domain that only contains $\sigma$; otherwise, there exists an axiom $S(c)$ in your subset such that the axiom $\neg S(\sigma)$ is not included in your subset, in which case interpret $\sigma$ as the same object that $c$ is interpreted as. Whatever finite subset of the theory is chosen, there should exist a structure defined in this fashion which models that subset.
This contradicts the compactness theorem. Therefore, $T \cup \neg T$ could not actually be a first-order theory. But since $\phi(x)$ is the only thing in the theory which hasn't been expressed directly with a first-order sentence, it follows that $\phi(x)$ must not be expressible in unsorted FOL.
Is my reasoning correct here? If so does this imply that unsorted FOL is not capable of simulating infinitely-many-sorted FOL, as a consequence of the compactness theorem, and that the latter is therefore more expressive?
If we had infinitely many sorts $\tau_1, \tau_2, \ldots$, why not add an infinite collection of unary predicates $S_1, S_2, \ldots$, add axioms for all $i \not = j$: $$ (\exists x) S_i(x) \\ S_i(x) \to \lnot S_j(x) $$ along with the axioms for constants of particular sorts, and replace each quantifier $(\exists x^{\tau_i}) \ldots$ with $(\exists x)[S_i(x) \land \ldots]$ and similarly for $(\forall x^{\tau_i})$. For notation, say that this interpretation takes a sentence $\phi$ in infinitely many sorts to $\phi^*$ in one sort with new unary relations.
This seems to interpret any model with infinitely many sorts into a model of the expanded theory with only one sort. Conversely, a model in the new language and expanded theory might have some elements that do not satisfy $S_i$ for any $i$, but if we discard those then the resulting model immediately leads to an equivalent model in infinitely many sorts. The elements that are not in any sort are irrelevant to sentences of the form $\phi^*$, because the quantifiers in $\phi^*$ are explicitly tied to particular sorts.
Letting $T^*$ be the interpretation and expansion of a theory $T$, in this way we still have that $T$ has a model with infinitely many sorts if and only if $T^*$ has a model with one sort.