In Kleene ''Introduction to Metamathematics'' 1971 on pp.420 he shows that if we have a formal system which for some formula $M(x)$ can prove the statement $\exists x M(x)$ then one can introduce a new formal system with one more sort of variables and corresponding new axioms and axiom schemata where the newly added sort intuitively corresponds to objects for which $M(x)$ is valid. Then one can show that this new sort is eliminable in a sense that new obtained formal system is equivalent to the previous one because there is an effective (computable) process of translation of formulas and certain provability conditions between formulas of different systems hold.
Now, I am interested in the reverse process. Assume we have some formal theory that has more than one sort of variables. Is it possible to reduce the number of sorts such that the resulting formal system is in some sense equivalent to the original one? I tried looking it up in books and on the internet, but could not find precise statements about this. For example, one idea that I found is that for each sort that wants to be removed I can just add a new predicate which intuitively represents the statement "this object is (was) from this sort". But I am not sure how to make it precise, especially what would be the precise definition of the new formal system being equivalent to the original one. I know that I want the new system to be intuitively not stronger and not weaker.
For example, in Kleene's book when he decides on the definition of equivalence he imposes one of the conditions to be that if $E$ is formula in the new system $S_2$ and $E'$ is the corresponding translation back to formal system $S_1$ then $E \iff E'$ is provable in $S_2$. But I do not see how that can work in the current situation because consider expression that contains the sort I want to eliminate. Then, it is a formula in $S_1$ but is not a formula in $S_2$ (because it does not contain that sort anymore). So, $E \iff E'$ cannot even be expressed in $S_2$. Similarly, if there is a formula that has a new predicate symbol that expresses that some variable is a member of some sort using newly defined predicate then this is expressible in $S_2$ but is not expressible in $S_1$, so $E \iff E'$ cannot be expressed in $S_1$ as well.
I hope I made my intentions clear and please let me know what you think about it. I would appreciate any kind of help, advice, references and so on.