Reduction of potentially-infinitely-many-sorted FOL to unsorted FOL:
For each sort Sn, add a constant symbol sn to the language
Add symbols:
 isSort\1
 isObject\1
 hasSort\2
For each sort symbol sn, add an axiom
 isSort(sn).
For each object symbol o, add an axiom
 isObject(o).
Add an axiom that everything is either a sort or an object:
 all x, isSort(x) v isObject(x).
Add an axiom that nothing is both a sort and an object:
 ~(exists x, isSort(x) ^ isObject(x)).
Add an axiom that every object has a sort:
 all x, isObject(x) -> (exists y, hasSort(x,y))
Add an axiom that only objects and sorts are in the hasSort relation:
 all x,y, hasSort(x,y) -> (isObject(x) & isSort(y))
Add an axiom that states that no object has multiple sorts
 need equality to assert cardinality?
 not quite:
 all x,s1,s2, (hasSort(x,s1) & hasSort(x,s2)) <-> (all y, hasSort(y,s1) <-> hasSort(y,s2))