I understand that the expressive power of first order logic with one sort is the same as any many sorted first order logic, and that higher order logic with general semantics is the same as a many sorted first order logic. You can add additional predicates to stratify these sorts and reduce many sorted first order logic to the orthodox classical single sorted first order logic. This looks pretty useful for reasoning about the logic itself, like establishing completeness and soundness hold, at the cost of readability.
But it looks to me that having these additional sorts with comprehension axioms can not only be more readable but be more compact; If you can prove things about families of functions or predicates in higher order logic (Henkin semantics) then you don't have to have lemmas for every single function and predicate referenced, but just one. There might be increased cost in unification across different but unifiable sorts, but I imagine the proof might be shorter.
Is this intuition accurate? Is many-sorted first order logic more efficient in proof length than single sorted first order logic?