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

TL;DR

This paper develops a complete and decidable logical theory for an expanded integer structure with a function based on a Beatty sequence, specifically when the parameter is a transcendental number.

Contribution

It introduces a model-complete axiomatization for the structure involving a Beatty sequence function with a transcendental parameter, ensuring decidability when the parameter is computable.

Findings

The theory is model-complete and fully axiomatizes the structure.

Decidability is achieved for computable transcendental parameters.

The work extends understanding of adding functions related to multiplication without losing decidability.

Abstract

We introduce a model-complete theory which completely axiomatizes the structure $Z_{\alpha}=(Z, +, 0, 1, f)$ where $f : x \to \lfloor{\alpha} x \rfloor $ is a unary function with $\alpha$ a fixed transcendental number. When $\alpha$ is computable, our theory is recursively enumerable, and hence decidable as a result of completeness. Therefore, this result fits into the more general theme of adding traces of multiplication to integers without losing decidability.