# Interesting fragments of first-order logic induced by sorting?

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.

• I must be missing something. As a special case, if you translate away sorts from a many-sorted language with just one sort, you obtain the original formula. In other words, your fragment is trivially the full first-order logic. Jun 3, 2014 at 10:30
• @EmilJeřábek It's probably me who's missing something. As far as I'm aware a formula like $\forall x.A$ where $x$ is of sort $S$, is translated into something like $\forall x.(P_S(x) \rightarrow A')$ where $A'$ is the corresponding translation of $A$ and $P_S$ is a predicate that formalises that something is in the sort $S$. I agree that in the special case of one sort that amounts to original FOL, but let's exclude that special case. I have edited the question accordingly. Jun 3, 2014 at 10:36
• Well, if you do not require the translated sorts to exhaust the universe, you get the full first-order logic on a subset of the universe defined by a predicate. The principle is the same, this is still computationally as difficult as the first-order logic itself. In other words, since the translation needs to be faithful in the first place, you cannot get anything easier than (many-sorted) first-order logic. Jun 3, 2014 at 10:45
• You shouldn’t think of many-sorted logic as a fragment of one-sorted logic. It is actually an extension of one-sorted logic, and what the translation tells you is that this extension is inessential. Jun 3, 2014 at 10:49
• @EmilJeřábek That's a good point. What I'm working with is (simpifying things a great deal) a many-sorted modal logic. I have empirical evidence that decision complexity is better than without sorting. I'm trying to organise my thoughts about this and am looking for related work. Jun 3, 2014 at 10:51