Alternation hierarchies of first order logic with regular predicates

Abstract

We investigate the decidability of the definability problem for fragments of first order logic over finite words enriched with regular numerical predicates. In this paper, we focus on the quantifier alternation hierarchies of first order logic. We obtain that deciding this problem for each level of the alternation hierarchy of both first order logic and its twovariable fragment when equipped with all regular numerical predicates is not harder than deciding it for the corresponding level equipped with only the linear order. Relying on some recent results, this proves the decidability for each level of the alternation hierarchy of the two-variable first order fragment while in the case of the first order logic the question remains open for levels greater than two. The main ingredients of the proofs are syntactic transformations of first-order formulas as well as the infinitely testable property, a new algebraic notion on varieties that we define.