Counting Modulo Quantifiers on Finite Structures

AbstractWe give a combinatorial method for proving elementary equivalence in first-order logic FO with counting modulo n quantifiers Dn. Inexpressibility results for FO(Dn) with built-in linear order are also considered. For instance, the class of linear orders of length divisible by n+1 cannot be expressed in FO(Dn). Using this result we prove that comparing cardinalities or connectivity of ordered graphs are not definable in FO(Dn). We also show that the height of complete n-ary trees cannot be expressed in FO(Dn) with linear order. Interpreting the predicate y=nx as a complete n-ary tree, we show that the predicate y=px cannot be defined in FO(Dn) with linear order, whenever p has a prime factor that does not divide n. This solves the problem raised by Niwiński and Stolboushkin (LICS '93). We also discuss a connection between our results and the well-known open problem in circuit complexity theory, whether ACC=NC1