The expressive power of existential first order

The aim of this paper is to study the first order theory of the successor, interpreted on finite words. More specifically, we complete the study of the hierarchy based on quantifier alternations (or Σnhierarchy). It was known (Thomas, 1982) that this hierarchy collapses at level 2, but the expressive power of the lower levels was not characterized effectively. We give a semigroup theoretic description of the expressive power of Σ1, the existential formulas, and BΣ1, the boolean combinations of existential formulas. Our characterization is algebraic and makes use of the syntactic semigroup, but contrary to a number of results in this field, is not in the scope of Eilenberg’s variety theorem, since BΣ1-definable languages are not closed under residuals. An important consequence is the following: given one of the levels of the hierarchy, there is polynomial time algorithm to decide whether the language accepted by a deterministic n-state automaton is expressibl