Generalized quantifiers and pebble games on finite structures (Q1892941)

\(L^k_{\infty \omega}\), \(k \geq 1\), is an infinitary logic that allows infinite cojunctions and disjunctions, but has only a total of \(k\) distinct variables. The authors study the family of infinitary logics \(L^k_{\infty \omega} (Q)\), where \(Q = \{Q_i : i \in I\}\) is a collection of simple unary generalized quantifiers on finite structures. This paper investigates the model-theoretic properties and the expressive powers of these infinitary logics on finite structures. For example, the authors show that by using appropriate pebble games one can tell whether or not two finite structures satisfy the same sentences of \(L^k_{\infty \omega} (Q)\) (a game-theoretic characterization of equivalence). Pebble games are applied to obtain a structural characterization of counting quantifiers. The main technical result is that there are natural polynomial-time properties on finite structures that are expressible by sentences of \(L^2_{\infty \omega} (C)\), where \(C\) denotes the counting quantifiers, which are not expressible by sentences of \(L^k_{\infty \omega} (Q)\), where \(Q\) is a finite sequence of arbitrary simple unary generalized quantifiers and \(k\) is a positive integer. The proof requires sophisticated combinatorial tools. The paper ends with a section on abstract finite model theory.