Model-completeness and decidability of the additive structure of integers expanded with a function for a Beatty sequence

Abstract

We introduce a model-complete theory which completely axiomatizes the structure Zα=〈Z,+,0,1,f〉 where f:x↦⌊αx⌋ is a unary function with α a fixed transcendental number. Moreover, we show that decidability of Zα is equivalent to computability of α. This result fits into the more general theme of adding traces of multiplication to integers without losing decidability. © 2024 Elsevier B.V.