Lindstrom theorems characterize logics in terms of model-theoretic conditions such as Compactness and the Lowenheim-Skolem property. Most existing Lindstrom theorems concern extensions of first-order logic. 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 challenging, as most known techniques rely on coding arguments that seem to require the full expressive power of first-order logic. In this paper, we provide Lindstrom characterizations for a number of fragments of first-order logic. These include the k-variable fragments for k ge 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. Characterizing the 2-variable fragment or the full guarded fragment remain open problems.
展开▼
机译：Lindstrom定理根据模型理论条件（例如紧凑性和Lowenheim-Skolem属性）来表征逻辑。现有的大多数Lindstrom定理都涉及一阶逻辑的扩展。另一方面，许多与计算机科学有关的逻辑是一阶逻辑的片段或片段的扩展，例如，k变量逻辑和各种模态逻辑。由于大多数已知技术都依赖于编码参数，而这些参数似乎需要一阶逻辑的完整表达能力，因此找到这些语言的Lindstrom定理可能具有挑战性。在本文中，我们为许多一阶逻辑片段提供了Lindstrom刻画。这些包括k ge 2的k变量片段，Tarski的关系代数，分级模态逻辑和二进制保护的片段。我们使用两种不同的证明技术。一种是对原始Lindstrom证明的修改。另一个涉及模态概念：双仿真，树展开和有限深度。我们的结果还暗示了语义保留定理。表征2变量片段或完整的受保护片段仍然是未解决的问题。
展开▼
