Counting module quantifiers on finite linearly ordered trees

We give a combinatorial method for proving elementary equivalence in first-order logic FO with counting module n quantifiers Dn. Inexpressibility results for FO(Dn) with built-in linear order are also considered. We show that certain divisibility properties of word models 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=(n+1)x cannot be defined in FO(Dn) with linear order. This proves the conjecture of Niwinski and Stolboushkin (1993). We also discuss connection between our results and the well-known open problem in circuit complexity theory, whether ACC=NC1