Logic in Computer Science (LICS 1996)

Paper: On the expressive power of variable-confined logics (at LICS 1996)

Authors: Phokion G. Kolaitis Moshe Y. Vardi

Abstract

In this paper we study the comparative expressive power of variable-confined logics, that is, logics with a fixed finite number of variables. This is motivated by the fact that the number of variables is considered a logical resource in descriptive complexity theory. We consider the expressive power of the logics FO/sup k/ (first-order logic with k variables), LFP/sup k/ (LFP with k variables, appropriately defined), and /spl Lscr//sub /spl infin/w//sup k/ (infinitary logic with k variables) over classes of finite structures. While the definitions of FO/sup k/ and /spl Lscr//sub /spl infin/w//sup k/ are quite clear, it turns out that ramifying LFP is a more delicate matter. We define LFP/sup k/ in terms of systems of least fixpoints, i.e., instead of taking the least fixpoint of a single positive first-order formula, we consider simultaneous least fixpoints of a vector of positive first-order formulas. As evidence that LFP/sup k/, k/spl ges/1, is the right ramification of LFP we offer two main results. The first is a new proof of a theorem by A. Dawar et al. (1995) to the effect that equivalence classes of finite structures with respect to the logic /spl Lscr//sub /spl infin/w//sup k/ are expressible in FO/sup k/. The second result, novel and technically difficult, is a characterization for each k/spl ges/1 of the collapse of /spl Lscr//sub /spl infin/w//sup k/ to FO/sup k/ in terms of boundedness of LFP/sup k/. More precisely, we establish the following stronger version of McColm's second conjecture: /spl Lscr//sub /spl infin/w//sup k/=FO/sup k/ on a class C of finite structures if and only if LFP/sup k/ is uniformly bounded on C.

BibTeX

  @InProceedings{KolaitisVardi-Ontheexpressivepowe,
    author = 	 {Phokion G. Kolaitis and Moshe Y. Vardi},
    title = 	 {On the expressive power of variable-confined logics},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {348-359},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }