Existential Definability of Unary Predicates in Buchi Arithmetic

The paper provides a complete characterisation of the sets S subset of N that are existentially definable in the structure < N; 0, 1,+, V-k, <=> (existential k-Buchi arithmetic), where for a fixed integer base k >= 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 Sigma(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 C-l,C- m comprise the languages {w} and w* for every word w is an element of{0, ..., k-1}* of length at most l, and the languages Sigma(l',m',c') for every triple l', m', c' satisfying l' <= l, m' <= m, c' is an element of [1..m']. Then a set S subset of N is existentially definable in k-Buchi 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 C-l,C-m.