One quantifier alternation in first-order logic with modular predicates

© 2015 EDP Sciences. Adding modular predicates yields a generalization of first-order logic FO over words. The expressive power of FO[ < , MOD] with order comparison x < y and predicates for x ≡ i mod n has been investigated by Barrington et al. The study of FO[ < , MOD]-fragments was initiated by Chaubard et al. More recently, Dartois and Paperman showed that definability in the two-variable fragment FO 2 [ < , MOD] is decidable. In this paper we continue this line of work. We give an effective algebraic characterization of the word languages in Σ 2 [ < , MOD]. The fragment Σ 2 consists of first-order formulas in prenex normal form with two blocks of quantifiers starting with an existential block. In addition we show that Δ 2 [ < , MOD], the largest subclass of Σ 2 [ < , MOD] which is closed under negation, has the same expressive power as two-variable logic FO 2 [ < , MOD]. This generalizes the result FO 2 [ < ] = Δ 2 [ < ] of Thérien and Wilke to modular predicates. As a byproduct, we obtain another decidable characterization of FO 2 [ < , MOD].