Existential Definability of Unary Predicates in Büchi Arithmetic

The paper provides a complete characterisation of the sets \(S\subseteq \mathbb {N}\) that are existentially definable in the structure \(\langle \mathbb {N};0,1,+,V_{k},\le \rangle \) (existential k-Büchi arithmetic), where for a fixed integer base \(k\ge 2\) the predicate \(V_k(x,y)\) is true whenever y is the greatest power of k dividing x. A quantifier elimination approach enables us to describe such sets in terms of regular expressions with a special language \(\varSigma _{l,m,c}\) . For every triple of positive integers l, m, c, this language is defined as the set of all k-ary representations of non-negative integers congruent to c modulo m with bit-length divisible by l. For a pair of integers \(l,m>0\) , let the class \(\mathscr {C}_{l,m}\) comprise the languages \(\{w\}\) and \(w^*\) for every word \(w\in \{0,...,k-1\}^{*}\) of length at most l, and the languages \(\varSigma _{l',m',c'}\) for every triple \(l',m',c'\) satisfying \(l'\le l\) , \(m'\le m\) , \(c'\in [1..m']\) . Then a set \(S\subseteq \mathbb {N}\) is existentially definable in k-Büchi arithmetic if and only if there exist positive integers l and m such that S can be obtained by a finite number of applications of concatenation and union to languages in \(\mathscr {C}_{l,m}\) .