Lindström theorems for fragments of first-order logic

Lindstrom theorems characterize logics in terms of model-theoretic conditions such as Compactness and the Lowenheim-Skolem property. Most existing characterizations of this kind concern extensions of first-order logic. But on the other hand, many logics relevant to computer science are fragments or extensions of fragments of first-order logic, e. g., k-variable logics and various modal logics. Finding Lindstrom theorems for these languages can be on coding arguments that seem to require the full expressive power of first-order logic. In this paper, we provide Lindstrom theorems for several fragments of first-order logic, including the k-variable fragments for k > 2, Tarski's relation algebra, graded modal logic, and the binary guarded fragment. We use two different proof techniques. One is a modification of the original Lindstrom proof. The other involves the modal concepts of bisimulation, tree unraveling, and finite depth. Our results also imply semantic preservation theorems.