Adding sort of sets over theory with multiple sorts? It's relatively standard to add a sort of sets over some base theory and supplement the axioms with comprehension principles as in second order arithmetic.
Is there a nice way to do this if your initial theory has multiple sorts?  For instance, if you started with a theory with a sort for natural numbers and a sort for reals?
Of course, one could introduce comprehension axioms that require a formula for each sort but that seems kinda ugly and I don't see how to extend that to infinitely many sorts.  Alternatively, one could define sorts for each finite (or more) product of sorts whose elements are members of that product but  I wonder if but you lose some degree of power w/o sets containing both kinds of elements?
Thats a little vague but if I knew how to state it formally I wouldn't be asking.
Is there some elegant approach I'm unaware of for this kind of thing?
 A: Let me argue that some care is needed, since one approach that might naively seem reasonable at first is definitely less powerful than we might desire.
Namely, what I claim is that it is strictly less powerful to allow second-order resources only over each sort separately, without any second-order relations spanning the sorts.
Let me prove this by illustrating with an example that my PhD student Nuno Maia and I had made a few years ago. Namely, consider the two-sorted model consisting of two copies of the standard model of arithmetic
$$\langle\newcommand\N{\mathbb{N}}\N_0,+_0,\cdot_0,<_0,\N_1,+_1,\cdot_1,<_1\rangle$$
That is, each $\N_i$ is the standard model $\N$, with the usual addition and multiplication structure. Let us assume that each sort has its own separate quantifiers and variable symbols, which is one of the standard ways to treat sorts.
We can prove that every first-order assertion $\varphi(\vec x,\vec y)$ in this two-sorted langauge, where the variables in $\vec x$ have sort $0$ and those in $\vec y$ have sort $1$, is equivalent to a Boolean combination of assertions $\varphi_0(\vec x)$ about the sort $0$ part only and assertions $\varphi_1(\vec y)$ solely about the sort $1$ part. This is true for atomic assertions and is preserved by Boolean combinations, and by quantifiers, precisely because the quantifiers are themselves sorted.
In particular, one cannot define the isomorphism of $\N_0$ with $\N_1$ in the two-sorted structure, since the isomorphism cannot be pulled apart this way into separate statements about the domain and range.
Now, the interesting further observation is that if one adds the second-order resources, but only to each sort separately, then you still can't define the isomorphism. That is, let's add sorted second-order quantifiers, with sort $0$ quantifiers quantifying over subsets and relations on $\N_0$ only, and others for second-order subsets and relations on $\N_1$. The point is that the induction argument still goes through.
In particular, and this was our main focus, one cannot prove the Dedekind categoricity proof in sorted second-order logic. That is, we can have a two-sorted model
$$\langle\N_0,+_0,\cdot_0,<_0,\N_1,+_1,\cdot_1,<_1\rangle$$
where each sort $\N_i$ satisfies the second-order Peano axioms, but there is no second-order definable isomorphism between them, if the second-order resources are contained in each sort separately.
This example is just the sort of recursive-definition situation that you describe in your question and comment, since the full categoricity argument of Dedekind is an induction in second-order logic.
That is, for the full categoricity result, which shows that there is only one model of second-order PA up to isomorphism, one uses the second-order resource spanning the sorts. Namely, one refers to the various partial isomorphisms that match the initial segments of one model with the other, and then prove (by second-order induction) that these cohere and that one can extend the to the first-point missed on either side, so collectively they define an isomorphism.
