On nonstandard models of Büchi Arithmetic

Büchi Arithmetic is the elementary theory of the natural numbers equipped with addition and the function $V_k$, which sends $x$ to the largest power of a fixed base $k \geqslant 2$ dividing $x$. This structure is automatic, and in fact it is universal among all automatic structures with respect to interpretations. However, A. Zapryagaev showed that an analogue of Tennenbaum's theorem holds here as well: Büchi Arithmetic admits no nonstandard automatic models. This raises the natural question of what nonstandard models — decidable ones in particular — Büchi Arithmetic does have, and how complex such models can be. In this work, we give an explicit construction of nonstandard models of Büchi arithmetic, yielding countably many nonstandard decidable models, as well as continuum many nonstandard countable models.