Paper: Lindström theorems for fragments of first-order logic (at LICS 2007)

Authors: Balder ten Cate Johan van Benthem Jouko A. Väänänen

Abstract

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.

BibTeX

  @InProceedings{tenCatevanVnnen-Lindstrmtheoremsfor,
    author = 	 {Balder ten Cate and Johan van Benthem and Jouko A. Väänänen},
    title = 	 {Lindström theorems for fragments of first-order logic},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {280--289},
    location =   {Wroclaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }