Abstract:
Büchi arithmetics $\mathrm{BA}_n$, $n\ge2$, are extensions of Presburger arithmetic with an unary functional symbol $V_n(x)$ denoting the largest power of $n$ that divides $x$. Definability of a set in $\mathrm{BA}_n$ is equivalent to its recognizability by a finite automaton receiving numbers in their $n$-ary expansion. We consider the interpretations of Presburger Arithmetic in the standard model of $\mathrm{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.