On Interpretations of Presburger Arithmetic in Buchi Arithmetics

Buchi arithmetics BA(n), n >= 2, are extensions of Presburger arithmetic with an unary functional symbol V-n(x) denoting Presburger arithmetic the largest power of n that divides x. Definability of a set in BA(n) is equivalent to its recognizability by a finite automaton receiving numbers in their n-ary expansion. We consider the interpretations of in the standard model of BA(n) and show that each such interpretation has an internal model isomorphic to the standard one. This answers a question by A. Visser on the interpretations of certain weak arithmetical theories in themselves.