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

TL;DR

The paper constructs a model-complete theory $\mathcal{T}_\alpha$ that axiomatizes the additive structure of the integers expanded by the Beatty-like function $f(x)=\lfloor \alpha x\rfloor$ for fixed transcendental $\alpha$. When $\alpha$ is computable, $\mathcal{T}_\alpha$ is recursively enumerable, making $\mathcal{Z}_\alpha$ decidable via completeness; the authors separate the analysis into non-algebraic and algebraic formulas and prove an Extended Kronecker lemma to reduce solvability of non-algebraic systems to quantifier-free checks. A key technical contribution is the Technical Trick, which reduces multi-variable algebraic equations to simpler non-algebraic forms, establishing model-completeness and, under computability of $\alpha$, decidability. The work also discusses the nature of definable sets—structured, random, and hybrid—and connects the non-algebraic fragment to an o-minimal-like theory $T^*$, suggesting a broad, density-driven picture of definability in this Beatty-augmented integer structure. Open questions remain about decidability and model-completeness in richer languages and for augmented orderings.

Abstract

We introduce a model-complete theory which completely axiomatizes the structure $Z_α=(Z, +, 0, 1, f)$ where $f : x \to \lfloorα x \rfloor $ is a unary function with $α$ a fixed transcendental number. When $α$ 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.

Theorems & Definitions (52)

• Proposition 1.1
• proof
• Proposition 1.3
• proof
• Lemma 2.1
• proof
• Remark 2.2
• Lemma 2.3
• proof
• Corollary 2.4