RAIRO-Theor. Inf. Appl.
Volume 49, Number 1, January-March 2015
|Page(s)||1 - 22|
|Published online||18 February 2015|
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
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.