In this paper (except in Section 5) all quantifiers are assumedto be so called simple unaryquantifiers, and all models are assumedto be finite. We give a necessary and sufficientcondition for a quantifier to be definablein terms of monotone quantifiers. For amonotone quantifier we give a necessaryand sufficient condition for beingdefinable in terms of a given set of bounded monotonequantifiers. Finally, we give a necessaryand sufficient condition for a monotonequantifier to be definable in terms of agiven monotone quantifier.Our analysis shows that (...) the quantifierat least one half and its relatives behavedifferently than other monotone quantifiers. (shrink)

A combinatorial criterium is given when a monadic quantifier is expressible by means of universe-independent monadic quantifiers of width n. It is proved that the corresponding hierarchy does not collapse. As an application, it is shown that the second resumption (or vectorization) of the Hartig quantifier is not definable by monadic quantifiers. The techniques rely on Ramsey theory.

First-order logic is known to have a severely limited expressive power on finite structures. As a result, several different extensions have been investigated, including fragments of second-order logic, fixpoint logic, and the infinitary logic L∞ωω in which every formula has only a finite number of variables. In this paper, we study generalized quantifiers in the realm of finite structures and combine them with the infinitary logic L∞ωω to obtain the logics L∞ωω, where Q = {Qi: iε I} is a family (...) of generalized quantifiers on finite structures. Using the logics L∞ωω, we can express polynomial-time properties that are not definable in L∞ωω, such as “there is an even number of x” and “there exists at least n/2 x” , without going to second-order logic. We show that equivalence of finite structures relative to L∞ωω can be characterized in terms of certain pebble games that are a variant of the Ehrenfeucht—Fraïssé games. We combine this game-theoretic characterization with sophisticated combinatorial tools from Ramsey theory, such as van der Waerden's Theorem and Folkman's Theorem, in order to investigate the scope and limits of generalized quantifiers in finite model theory. We obtain sharp lower bounds for expressibility in the logics L∞ωω and discover an intrinsic difference between adding finitely many simple unary generalized quantifiers to L∞ωω adding infinitely many. In particular, we show that if Qis a finite sequence of simple unary generalized quantifiers, then the equicardinality, or Härtig, quantifier is not definable in L∞ωω. We also show that the query “does the equivalence relation E have an even number of equivalence classes” is not definable in the extension L∞ωω of L∞ωω by the Härtig quantifier I and any finite sequence Q of simple unary generalized quantifiers. (shrink)

The concept of a generalized quantifier of a given similarity type was defined in [12]. Our main result says that on finite structures different similarity types give rise to different classes of generalized quantifiers. More exactly, for every similarity type t there is a generalized quantifier of type t which is not definable in the extension of first order logic by all generalized quantifiers of type smaller than t. This was proved for unary similarity types by Per Lindström [17] with (...) a counting argument. We extend his method to arbitrary similarity types. (shrink)

The concept of a generalized quantifier of a given similarity type was defined in [12]. Our main result says that on finite structures different similarity types give rise to different classes of generalized quantifiers. More exactly, for every similarity typetthere is a generalized quantifier of typetwhich is not definable in the extension of first order logic by all generalized quantifiers of type smaller thant. This was proved for unary similarity types by Per Lindström [17] with a counting argument. We extend (...) his method to arbitrary similarity types. (shrink)

We consider the problem of finding a characterization for polynomial time computable queries on finite structures in terms of logical definability. It is well known that fixpoint logic provides such a characterization in the presence of a built-in linear order, but without linear order even very simple polynomial time queries involving counting are not expressible in fixpoint logic. Our approach to the problem is based on generalized quantifiers. A generalized quantifier isn-ary if it binds any number of formulas, but at (...) mostnvariables in each formula. We prove that, for each natural numbern, there is a query on finite structures which is expressible in fixpoint logic, but not in the extension of first-order logic by any set ofn-ary quantifiers. It follows that the expressive power of fixpoint logic cannot be captured by adding finitely many quantifiers to first-order logic. Furthermore, we prove that, for each natural numbern, there is a polynomial time computable query which is not definable in any extension of fixpoint logic byn-ary quantifiers. In particular, this rules out the possibility of characterizing PTIME in terms of definability in fixpoint logic extended by a finite set of generalized quantifiers. (shrink)

A combinatorial criterium is given when a monadic quantifier is expressible by means of universe-independent monadic quantifiers of width n. It is proved that the corresponding hierarchy does not collapse. As an application, it is shown that the second resumption of the Hartig quantifier is not definable by monadic quantifiers. The techniques rely on Ramsey theory.