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

Basic Information

• Paper ID: 2110.01673
• Title: Model-completeness and decidability of the additive structure of integers expanded with a function for a Beatty sequence
• Authors: Mohsen Khani, Ali N. Valizadeh, Afshin Zarei
• Classification: math.LO (Mathematical Logic)
• Publication Date: April 17, 2024 (final version)
• Paper Link: https://arxiv.org/abs/2110.01673

Abstract

This paper introduces a model-complete theory that fully axiomatizes the structure $Z_α = ⟨Z, +, 0, 1, f⟩$, where $f : x ↦ ⌊αx⌋$ is a unary function and $α$ is a fixed transcendental number. When $α$ is computable, the theory is recursively enumerable, and consequently decidable as a result of completeness. This result aligns with the broader theme of adding multiplicative traces to the integers without losing decidability.

Research Background and Motivation

Problem Background

1. Core Problem: Investigating the decidability of expanded structures of the additive group of integers $⟨Z, +⟩$, particularly the structural properties after adding the Beatty sequence function $f(x) = ⌊αx⌋$.
2. Research Significance:
   • Lies at the intersection of two active research directions: on one hand, decidability and classification (stable or unstable structures) of expansions of $⟨Z, +⟩$
   • On the other hand, research on expansions of the real line with specific discrete additive subgroups
3. Limitations of Existing Work:
   • Hieronymi H16 only proved decidability for quadratic $α$
   • For transcendental $α$, the decidability of the more general structure $R_α$ remains unresolved
   • New techniques are needed to handle the independence of different powers of $f$ in the transcendental case
4. Research Motivation:
   • Provide a decidability proof for the transcendental case
   • Give a constructive proof using fundamental tools from model theory and number theory
   • Lay the foundation for resolving the more general $R_α$ structure problem

Core Contributions

1. Established a model-complete theory: Constructed the theory $T_α$ that fully axiomatizes the structure $Z_α = ⟨Z, +, 0, 1, f⟩$, where $f(x) = ⌊αx⌋$ and $α$ is transcendental.
2. Proved decidability: When $α$ is computable, $T_α$ is recursively enumerable, and combined with completeness yields decidability.
3. Technical Innovation:
   • Transformed fractional part relations into first-order logic formulas
   • Employed an extended Kronecker lemma to handle non-algebraic formulas
   • Developed reduction techniques for handling algebraic formulas
4. Theoretical Analysis: Proved that the structure possesses strict order properties and analyzed the structure of definable sets.

Detailed Methodology

Task Definition

Study the first-order theory of the structure $Z_α = ⟨Z, +, 0, 1, f⟩$ in the language $L = \{+, -, 0, 1, f\}$, where:

• $Z$ is the set of integers
• $+$ is the addition operation
• $f: x ↦ ⌊αx⌋$ is the Beatty sequence function
• $α$ is a fixed computable transcendental number

Core Technical Framework

1. Logical Expression of Fractional Parts

Key Observation: Although fractional parts are not in the language, key properties of fractional parts can be described in $L$ as follows:

For $a, b ∈ Z$ and $n ∈ N$:

• $f(na) = nf(a) + i$ if and only if $\frac{i}{n} < [αa] < \frac{i+1}{n}$
• $[αa] + [αb] < 1$ if and only if $f(a+b) = f(a) + f(b)$
• $[αa] < [αb]$ if and only if $f(b-a) = f(b) - f(a)$

where $[x] = x - ⌊x⌋$ denotes the fractional part.

2. Formula Classification Strategy

Systematically partition $L$-formulas into two classes:

Non-algebraic formulas: Of the form $\sum_{i=0}^{\ell_1} n_{1i}[αf^i(x_1)] + \cdots + \sum_{i=0}^{\ell_k} n_{ki}[αf^i(x_k)] \triangleleft \sum_{i=0}^{k'} m_i[αy_i] + [αq] + \ell$

Algebraic formulas: Of the form $h_1(x_1) + \cdots + h_n(x_n) = y$, where $h_i(x)$ are $f$-polynomials.

3. Extended Kronecker Lemma

Theorem 3.4 (Extended Kronecker Lemma): For each $n ∈ N$, the following $(n+1)$-tuple set is dense in $(0,1)^{n+1}$: $\{([αa], [αf(a)], [αf^2(a)], \ldots, [αf^n(a)]) : a ∈ N\}$

This holds because the transcendence of $α$ ensures that $1, α, α^2, \ldots, α^n$ are linearly independent over $\mathbb{Q}$.

Model-Completeness Proof Strategy

Step 1: Handling Non-algebraic Formulas

• Lemma 3.6: For a set of non-algebraic formulas $Γ(x; \bar{y})$, there exists a quantifier-free formula $χ(\bar{y})$ such that $Z_α ⊨ ∀\bar{y}(∃xΓ(x; \bar{y}) ↔ χ(\bar{y}))$
• Apply the Fourier-Motzkin elimination algorithm to handle systems of linear inequalities

Step 2: Reduction Techniques

• Lemma 4.12 (Technical Trick): Reduce mixed systems containing algebraic formulas to non-algebraic systems with fewer variables
• Key idea: By introducing auxiliary variables $w$ and terms $h(x)$, transform multivariate algebraic equations into univariate cases

Step 3: Algebraic Closure

• Lemma 4.13: If $M_1 ⊆ M_2$ are models of $T_α$, $b ∈ M_1$, $a ∈ M_2$, and $h(a) = b$, then $a ∈ M_1$
• Ensures that substructures are closed under inverse operations of different powers of $f$

Axiomatization System

Axiom Scheme 1 (Computing $f(n)$)

For $n ∈ N$ and $0 ≤ i < n$ with $\frac{f(n)}{n} ≡ i$: $f(\underbrace{1 + \cdots + 1}_{n \text{ times}}) = \underbrace{f(1) + \cdots + f(1)}_{n \text{ times}} + \underbrace{1 + \cdots + 1}_{i \text{ times}}$

Axiom 2 (Basic Properties)

1. $∀x∀y(f(x+y) = f(x) + f(y) ∨ f(x+y) = f(x) + f(y) + 1)$
2. $∀x(f(-x) = -f(x) - 1)$
3. $∀y∃x(\bigvee_{i=0}^{f(1)} y + i = f(x))$
4. The relation $[αx] < [αy]$ is a dense linear order

Axiom Scheme 3 (Density)

For $m, n ∈ N$: If $\bigwedge_{i=1}^n [αz_i] < [αy_i]$, then there exist at least $m$ distinct $x$ such that $\bigwedge_{i=1}^n [αy_i] < [αf^i(x)] < [αz_i]$.

Experimental Results and Theoretical Analysis

Main Results

Main Theorem: Let $α$ be a transcendental real number. Then:

1. $T_α$ is a complete and model-complete axiomatization of the structure $Z_α$
2. $Z_α$ possesses strict order properties
3. When $α$ is computable, $T_α$ is decidable

Properties of Definable Sets

1. Structured Sets: Formulas not containing powers of $f$ define congruence classes (infinite arithmetic progressions)
2. Random Sets: Sets defined by formulas containing powers of $f$ do not contain infinite arithmetic progressions
3. Mixed Properties: The range of any $f$-polynomial contains finite arithmetic progressions of arbitrary length

Proposition 5.1: For $h(x) = \sum_{i=0}^k m_i f^i(x)$, for each $n ∈ N$, there exists an arithmetic progression of length $n$ in the range of $h$.

Related Work

1. Hieronymi H16: Proved decidability of $R_α$ for quadratic $α$
2. Conant & Pillay CP18: Studied stability classification of expansions of $⟨Z, +⟩$
3. Günaydin & Özsahakyan GO22: Independent research treating Beatty sequences as predicates rather than functions
4. Khani & Zarei KZ22: Simplified proof for the golden ratio case

Conclusions and Discussion

Main Conclusions

1. Successfully generalized Hieronymi's result from quadratic numbers to transcendental numbers
2. Provided a constructive proof of model-completeness
3. Established a new technical framework for handling transcendental cases

Limitations

1. Requires computability of $α$ to ensure recursive enumerability
2. The more general $R_α$ structure problem remains unresolved
3. Quantifier elimination appears infeasible in the transcendental case

Future Directions

1. Open Problem: Decidability and model-completeness of the structure $⟨Z, <, +, -, 0, 1, f⟩$ (with integer order added)
2. Generalization to other types of transcendental numbers
3. Investigation of more complex Beatty sequence combinations

Technical Innovation Points

1. Effective Model-Completeness: The proof process is constructive and allows effective quantifier elimination
2. o-Minimality Connection: Relationship between the non-algebraic part $T_{nalg}$ and o-minimal theories
3. Unified Framework: Unified approach for handling both algebraic and non-algebraic formulas

In-Depth Evaluation

Strengths

1. Theoretical Contribution: Significant generalization of known results, advancing from quadratic to transcendental numbers
2. Technical Innovation: Creative application of extended Kronecker lemma and well-designed reduction techniques
3. Method Generality: Techniques applicable to algebraic number cases
4. Constructive Proof: Provides effective model-completeness results

Weaknesses

1. Computational Complexity: Although theoretically decidable, practical complexity may be very high
2. Expressive Limitations: Cannot handle certain naturally related structures
3. Technical Complexity: Proofs involve multiple complex technical lemmas

Impact

1. Academic Value: Provides new techniques and results for mathematical logic and model theory
2. Application Prospects: Lays foundation for studying more complex arithmetic structures
3. Methodological Contribution: Demonstrates systematic approaches to handling mixed algebraic-analytic structures

Applicable Scenarios

1. Research on decidability theory in mathematical logic
2. Diophantine problems in arithmetic geometry
3. Automated theorem proving in computer science
4. Distribution properties in number theory

References

• H16 P. Hieronymi, Expansions of the ordered additive group of real numbers by two discrete subgroups
• KZ22 M. Khani and A. Zarei, The additive structure of integers with the lower Wythoff sequence
• HM+21 P. Hieronymi et al., Decidability for Sturmian words
• C60 I. G. Connell, Some properties of Beatty sequences II