2025-11-18T03:55:12.452739

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

Khani, Valizadeh, Zarei
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.
academic

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

基本信息

  • 论文ID: 2110.01673
  • 标题: Model-completeness and decidability of the additive structure of integers expanded with a function for a Beatty sequence
  • 作者: Mohsen Khani, Ali N. Valizadeh, Afshin Zarei
  • 分类: math.LO (数理逻辑)
  • 发表时间: 2024年4月17日 (最终版本)
  • 论文链接: https://arxiv.org/abs/2110.01673

摘要

本文引入了一个模型完备的理论，完全公理化了结构 Zα=⟨Z,+,0,1,f⟩Z_α = ⟨Z, +, 0, 1, f⟩，其中 f:x↦⌊αx⌋f : x ↦ ⌊αx⌋ 是一个一元函数，αα 是固定的超越数。当 αα 可计算时，该理论是递归可枚举的，因此作为完备性的结果是可判定的。这一结果符合在不失去可判定性的情况下向整数添加乘法痕迹的更一般主题。

研究背景与动机

问题背景

  1. 核心问题：研究整数加法群 ⟨Z,+⟩⟨Z, +⟩ 的扩张结构的可判定性，特别是添加Beatty序列函数 f(x)=⌊αx⌋f(x) = ⌊αx⌋ 后的结构性质。
  2. 研究意义：
    • 属于两个活跃研究方向的交叉：一方面涉及 ⟨Z,+⟩⟨Z, +⟩ 扩张的可判定性及其分类（稳定或不稳定结构）
    • 另一方面涉及实数线与特定离散加法子群的扩张研究
  3. 现有工作的局限性：
    • Hieronymi在H16中仅证明了二次数 αα 情况下的可判定性
    • 对于超越数 αα 的情况，更一般的结构 RαR_α 的可判定性尚未解决
    • 需要新的技术处理超越数情况下不同幂次 ff 的独立性
  4. 研究动机：
    • 提供超越数情况下的可判定性证明
    • 使用模型论和数论的基本工具给出构造性证明
    • 为解决更一般的 RαR_α 结构问题奠定基础

核心贡献

  1. 建立了模型完备理论：构造了理论 TαT_α，完全公理化了结构 Zα=⟨Z,+,0,1,f⟩Z_α = ⟨Z, +, 0, 1, f⟩，其中 f(x)=⌊αx⌋f(x) = ⌊αx⌋，αα 为超越数。
  2. 证明了可判定性：当 αα 可计算时，TαT_α 是递归可枚举的，结合完备性得到可判定性。
  3. 技术创新：
    • 将小数部分关系转化为一阶逻辑公式
    • 使用扩展的Kronecker引理处理非代数公式
    • 开发了处理代数公式的约简技术
  4. 理论分析：证明了该结构具有严格序性质，并分析了可定义集合的结构。

方法详解

任务定义

研究结构 Zα=⟨Z,+,0,1,f⟩Z_α = ⟨Z, +, 0, 1, f⟩ 在语言 L={+,−,0,1,f}L = \{+, -, 0, 1, f\} 中的一阶理论，其中：

  • ZZ 是整数集
  • ++ 是加法运算
  • f:x↦⌊αx⌋f: x ↦ ⌊αx⌋ 是Beatty序列函数
  • αα 是固定的可计算超越数

核心技术框架

1. 小数部分的逻辑表达

关键观察：虽然语言中没有小数部分，但可以通过以下方式在 LL 中描述小数部分的关键性质：

对于 a,b∈Za, b ∈ Z 和 n∈Nn ∈ N：

  • f(na)=nf(a)+if(na) = nf(a) + i 当且仅当 in<[αa]<i+1n\frac{i}{n} < [αa] < \frac{i+1}{n}
  • [αa]+[αb]<1[αa] + [αb] < 1 当且仅当 f(a+b)=f(a)+f(b)f(a+b) = f(a) + f(b)
  • [αa]<[αb][αa] < [αb] 当且仅当 f(b−a)=f(b)−f(a)f(b-a) = f(b) - f(a)

其中 [x]=x−⌊x⌋[x] = x - ⌊x⌋ 表示小数部分。

2. 公式分类策略

将 LL-公式系统分为两类：

非代数公式：形如 ∑i=0ℓ1n1i[αfi(x1)]+⋯+∑i=0ℓknki[αfi(xk)]◃∑i=0k′mi[αyi]+[αq]+ℓ\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

代数公式：形如 h1(x1)+⋯+hn(xn)=yh_1(x_1) + \cdots + h_n(x_n) = y，其中 hi(x)h_i(x) 是 ff-多项式。

3. 扩展Kronecker引理

定理3.4（扩展Kronecker引理）：对于每个 n∈Nn ∈ N，以下 (n+1)(n+1)-元组集合在 (0,1)n+1(0,1)^{n+1} 中稠密： {([αa],[αf(a)],[αf2(a)],…,[αfn(a)]):a∈N}\{([αa], [αf(a)], [αf^2(a)], \ldots, [αf^n(a)]) : a ∈ N\}

这是因为 αα 的超越性保证了 1,α,α2,…,αn1, α, α^2, \ldots, α^n 在 Q\mathbb{Q} 上线性无关。

模型完备性证明策略

步骤1：处理非代数公式

  • 引理3.6：对于非代数公式集合 Γ(x;yˉ)Γ(x; \bar{y})，存在量词自由公式 χ(yˉ)χ(\bar{y}) 使得 Zα⊨∀yˉ(∃xΓ(x;yˉ)↔χ(yˉ))Z_α ⊨ ∀\bar{y}(∃xΓ(x; \bar{y}) ↔ χ(\bar{y}))
  • 使用Fourier-Motzkin消元算法处理线性不等式系统

步骤2：约简技术

  • 引理4.12（技术技巧）：将包含代数公式的混合系统约简为较少变量的非代数系统
  • 关键思想：通过引入辅助变量 ww 和项 h(x)h(x)，将多变量代数方程转化为单变量情况

步骤3：代数封闭性

  • 引理4.13：若 M1⊆M2M_1 ⊆ M_2 是 TαT_α 的模型，b∈M1b ∈ M_1，a∈M2a ∈ M_2 且 h(a)=bh(a) = b，则 a∈M1a ∈ M_1
  • 保证了子结构在 ff 的不同幂次下的逆运算封闭性

公理化系统

公理方案1（计算 f(n)f(n)）

对于 n∈Nn ∈ N 和 0≤i<n0 ≤ i < n 且 f(n)n≡i\frac{f(n)}{n} ≡ i： f(1+⋯+1⏟n次)=f(1)+⋯+f(1)⏟n次+1+⋯+1⏟i次f(\underbrace{1 + \cdots + 1}_{n \text{次}}) = \underbrace{f(1) + \cdots + f(1)}_{n \text{次}} + \underbrace{1 + \cdots + 1}_{i \text{次}}

公理2（基本性质）

  1. ∀x∀y(f(x+y)=f(x)+f(y)∨f(x+y)=f(x)+f(y)+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)∀x(f(-x) = -f(x) - 1)
  3. ∀y∃x(⋁i=0f(1)y+i=f(x))∀y∃x(\bigvee_{i=0}^{f(1)} y + i = f(x))
  4. 关系 [αx]<[αy][αx] < [αy] 是稠密线性序

公理方案3（稠密性）

对于 m,n∈Nm, n ∈ N：如果 ⋀i=1n[αzi]<[αyi]\bigwedge_{i=1}^n [αz_i] < [αy_i]，则存在至少 mm 个不同的 xx 使得 ⋀i=1n[αyi]<[αfi(x)]<[αzi]\bigwedge_{i=1}^n [αy_i] < [αf^i(x)] < [αz_i]。

实验结果与理论分析

主要结果

主定理：设 αα 是超越实数，则：

  1. TαT_α 是结构 ZαZ_α 的完备且模型完备的公理化
  2. ZαZ_α 具有严格序性质
  3. 当 αα 可计算时，TαT_α 是可判定的

可定义集合的性质

  1. 结构化集合：不包含 ff 幂次的公式定义同余类（无限算术级数）
  2. 随机集合：包含 ff 幂次的公式定义的集合不包含无限算术级数
  3. 混合性质：任何 ff-多项式的值域都包含任意长度的有限算术级数

命题5.1：对于 h(x)=∑i=0kmifi(x)h(x) = \sum_{i=0}^k m_i f^i(x)，对于每个 n∈Nn ∈ N，hh 的值域中存在长度为 nn 的算术级数。

相关工作

  1. Hieronymi H16：证明了二次 αα 情况下 RαR_α 的可判定性
  2. Conant & Pillay CP18：研究 ⟨Z,+⟩⟨Z, +⟩ 扩张的稳定性分类
  3. Günaydin & Özsahakyan GO22：独立研究，将Beatty序列作为谓词而非函数处理
  4. Khani & Zarei KZ22：黄金比例情况的简化证明

结论与讨论

主要结论

  1. 成功将Hieronymi的结果从二次数推广到超越数
  2. 提供了构造性的模型完备性证明
  3. 建立了处理超越数情况的新技术框架

局限性

  1. 需要 αα 的可计算性来保证递归可枚举性
  2. 对于更一般的结构 RαR_α 问题尚未解决
  3. 量词消除在超越数情况下似乎不可行

未来方向

  1. 开放问题：结构 ⟨Z,<,+,−,0,1,f⟩⟨Z, <, +, -, 0, 1, f⟩（添加整数序）的可判定性和模型完备性
  2. 推广到其他类型的超越数
  3. 研究更复杂的Beatty序列组合

技术创新点

  1. 有效模型完备性：证明过程是构造性的，可以有效地进行量词消元
  2. o-极小连接：非代数部分 TnalgT_{nalg} 与o-极小理论的联系
  3. 统一框架：处理代数和非代数公式的统一方法

深度评价

优点

  1. 理论贡献：显著推广了已知结果，从二次数到超越数是重要进展
  2. 技术创新：扩展Kronecker引理的应用和约简技术的设计很有创意
  3. 方法通用性：技术可以应用于代数数情况
  4. 构造性证明：提供了有效的模型完备性结果

不足

  1. 计算复杂性：虽然理论上可判定，但实际复杂性可能很高
  2. 表达能力限制：无法处理某些自然的相关结构
  3. 技术复杂性：证明涉及多个复杂的技术引理

影响力

  1. 学术价值：为数理逻辑和模型论领域提供了新的技术和结果
  2. 应用前景：为研究更复杂的算术结构奠定了基础
  3. 方法论贡献：展示了如何系统地处理此类混合代数-分析结构

适用场景

  1. 数理逻辑中的可判定性理论研究
  2. 算术几何中的丢番图问题
  3. 计算机科学中的自动定理证明
  4. 数论中的分布性质研究

参考文献

  • 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