I read this question earlier today. It contains this comment by Noah Schweber, reproduced below, as well as this answer.
"Many-sorted logic can be easily rewritten into standard (one sort) predicate logic with suitable predicates." This is mostly true, but misses an important subtlety: namely, compactness fails for many-sorted logic with infinitely many sorts, since "every element has a sort" isn't a first-order-expressible principle but is built into the semantics for many-sorted logic.
I'm having trouble understanding why the argument holds. In the course of attempting to write a proof that many-sorted logic is compact given that first-order logic is compact, I think I've grasped the point that Noah was making originally, namely that the first-order equivalent of a many-sorted model may have domain elements with no sort (i.e. for which no sort predicate holds). I am failing, however, to see why this would make many-sorted logic non-compact. Intuitively, sortless entities seem like a kind of dark matter that doesn't interact with the semantics at all, since all functions, relations, constants, free, and bound variables are annotated with sorts and thus sortless entities never get a chance to influence the truth value of a well-formed formula.
So, is many-sorted logic compact? What am I missing?
What follows is my attempt to prove that many-sorted logic is compact
To make the intuition a little easier, let's assume that I have at least one sort and that all sorts are nonempty.
I'm pretty sure that first-order logic is compact, regardless of the size of the signature, even though you can do weird things with uncountable signatures like insist that the domain is uncountable using $\{c_\alpha \neq c_\beta : \alpha, \beta \in \kappa \land \alpha \neq \beta \}$ for some $|\kappa| > \omega$.
Let's assume I have a set of sentences in many-sorted logic that is finitely-satisfiable called $\Delta$. $\Delta$ might be satisfiable, it might not. At this point we don't know.
$\Delta$ can be converted into first-order logic (call the sentences $\Delta'$) by replacing each sort $S$ with a dedicated unary predicate $P$ and replacing quantifiers $[\forall x : S] ( \cdots )$ with circumlocutions like $[\forall x]( P(x) \to \cdots ) $ and then further insisting, for every distinct $i \neq j$, that $[\forall x](\lnot (P_i(x) \land P_j(x)))$. Additionally, for every function symbol, we have sentences asserting when their inputs have the correct sort, their output has the correct sort.
$\Delta$ is finitely satisfiable, so $\Delta'$ is finitely satisfiable. Thus $\Delta'$ is satisfiable. Thus $\Delta'$ has a model $M \models \Delta'$.
$M$ may contain what I will call sortless garbage, for which no unary-predicate-that's-a-sort-in-disguise $P$ holds.
Let $M'$ be the structure $M$ with all the sortless garbage removed. I claim that $M'$ is still a structure, i.e. none of the functions have become partial, because sortless garbage cannot be in the image of any function (this is where I'm using the assumption that all sorts are inhabited).
I claim that $M' \models \Delta'$ because all constant symbols refer to sorted entities and all quantifies are restricted to quantify exclusively over sorted entities.
$M'$ can be converted into $M''$, a many-sorted structure, in a straightforward way by interpreting the unary predicates as sorts again. For that many-sorted structure, $\Delta$ holds, as desired.