Paper: Ordering Finite Variable Types with Generalized Quantifiers (at LICS 1998)

Authors: Anuj Dawar Lauri Hella Anil Seth

Abstract

Let Q be a finite set of generalized quantifiers. By L^k(Q) we denote the k-variable fragment of FO(Q), first order logic extended with Q. We show that for each k, there is a PFP(Q)-definable linear pre-order whose equivalence classes in any finite structure 21 are the L^k(Q)-types in 21. For some special classes of generalized quantifiers Q, we show that such an ordering of L^k(Q)-types is already definable in IFP(Q). As applications of the above results, we prove some generalizations of the Abiteboul-Vianu theorem. For instance, we show that for any finite set Q of modular counting quantifiers, P=PSPACE if, and only if, IFP(Q)=PFP(Q) over finite structures. On the other hand, we show that an ordering of L ^k(Q)-types is not always definable in IFP(Q). Indeed, we construct a single, polynomial time computable quantifier P such that the equivalence relation ?^k,P, and hence ordering on L ^k(P)-types, is not definable in IFP(P)

BibTeX

  @InProceedings{DawarHellaSeth-OrderingFiniteVaria,
    author = 	 {Anuj Dawar and Lauri Hella and Anil Seth},
    title = 	 {Ordering Finite Variable Types with Generalized Quantifiers},
    booktitle =  {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)},
    year =	 {1998},
    month =	 {June}, 
    pages =      {28--43},
    location =   {Indianapolis, IN, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }