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 D_n. Inexpressibility results for FO(D_n) with built-in linear order are also considered. We show that certain divisibility properties of word models are not definable in FO(D_n ). We also show that the height of complete n-ary trees cannot be expressed in FO(D_n) 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(D_n) 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=NC¹