One quantifier alternation in first-order logic with modular predicates∗
Received: 17 October 2013
Accepted: 18 June 2014
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 ≡ imodn 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 FO2 [<,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 FO2 [<,MOD]. This generalizes the result FO2 [<] = Δ2 [<] of Thérien and Wilke to modular predicates. As a byproduct, we obtain another decidable characterization of FO2 [<,MOD].
Mathematics Subject Classification: 68Q70 / 03D05 / 20M35 / 68Q45
Key words: Finite monoid / syntactic homomorphism / logical fragment / first-order logic / modular predicate
© EDP Sciences 2015