In first approximation, modal logic (I'm using the term loosely) can be understood as an interesting fragment of first-order logic (for simplicity I ignore e.g. how modal logic relates to second-order logics) with bounded/local quantifiers: modal operators can be thought of as abbreviations that encode quantification over relationally-accessible states in a convenient, variable-free notation. The standard translation of modal logic into first-order logic gives rise to interesting fragments like the finite variable fragments, the fragments closed under bisimulation, guarded fragments that have been investigated heavily, etc. The standard translation also allow us to push techniques, constructions and results between logics.

Modal logic is used because formulae and proofs in modal logic are more succinct, sometimes substantially so, than the corresponding first-order fragments.

In a similar sense, many-sorted first-order logic can be seen as a fragment of first-order logic by translating sorts into appropriate first-order predicates. Here I assume that we have more than one sort. Now my question: are there non-trivial results about fragments of first-order logic obtained by translating away sorts? I'm particularly interested in questions about the complexity of decision problems.

PS: I'm not sure if this question is suitable for mathoverflow. If not, please feel free to close or move to a more appropriate venue.

fragmentof one-sorted logic. It is actually anextensionof one-sorted logic, and what the translation tells you is that this extension is inessential. $\endgroup$