We study an extension of first-order logic by modular quantifiers of a fixed modulus $q$. Drawing on collapse results from finite model theory and techniques of finite semigroup theory, we show that if the only available numerical predicate is addition, then sentences in this logic cannot define the set of bit strings in which the number of 1's is divisible by a prime $p$ that does not divide $q.$ More generally, we give an effective algebraic characterization of all the regular languages definable in this logic.
The same statement with addition replaced by arbitrary numerical predicates is equivalent to the conjectured separation of the circuit complexity classes $ACC$ and $NC^1.$ Thus our theorem can be viewed as proving a highly uniform version of this conjecture.
A preliminary version of this paper appeared in the proceedings of the 2006 STACS conference. The full paper has been accepted for publication in {\it SIAM Journal on Computing.}