Reduction of potentially-infinitely-many-sorted FOL to unisorted FOL via equivalence relation?
 * No way to define reflexive-symmetric-transitive closure
Add a binary relation symbol R
Assert R is reflexive:
 * all x, R(x,x)
Assert R is symmetric:
 * all x,y, R(x,y) -> R(y,x)
Assert R is transitive:
 * all x,y,z, R(x,y) -> R(y,z) -> R(x,z)
For each sort Sn, make a constant symbol sn
Add an isSort\1 relation symbol
For each sort symbol s, add the axiom:
 * isSort(s)
For every pair of sort symbols s, s', add the axiom:
 * ~R(s,s')
Add an axiom:
 * all x, exists s, isSort(s) ^ R(x,s)

Then to quantify over a sort s, you do:
 * all x, R(x,s), ...
 * exists x, R(x,s), ...

This avoids changing the models in a major way, so long as each sort is inhabited, because we can essentially interpret each sort object as being interpreted as some representative object in that sort (an object in the equivalence class that defines that sort). The only question really is what happens if many-sorted logic allows empty sorts in its interpretations, there would be nowhere for our constant sort-symbols to map to in the domain for these models.