💻 computer science

On existential Büchi arithmetic in two coprime bases

本文通过提供一个量词消去论证，确立了包含两个互质基底的 Büchi 谓词的扩展 Presburger 算术的存在量词片段的可判定性。

原作者： Joris Nieuwveld

发布于 2026-08-26

📖 1 分钟阅读☕ 轻松阅读

原作者： Joris Nieuwveld

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

长期以来，数学一直痴迷于支配数字的规则，特别是我们如何利用加法和排序等简单运算来描述它们。近一个世纪以来，一种被称为普雷斯伯格算术（Presburger arithmetic）的系统一直作为这项工作的可靠基础。它允许我们仅使用加法和“小于”的概念来对整数进行提问，并且得益于 1921 年开发的一种方法，我们知道在该系统中提出的任何问题都可以得到确定的“是”或“否”的回答。然而，这个系统是有限制的；它无法处理乘法，而乘法正是开启完整算术复杂性的钥匙。一旦加入乘法，该系统就会变得如此强大，以至于没有任何算法能够保证能回答每一个可能的问题。

为了弥合加法这一简单世界与乘法这一复杂世界之间的鸿沟，研究人员尝试向该系统添加特定的、受限的工具。其中一种工具是一种谓词，用于识别能够整除另一个数的特定基数的最大幂次。例如，如果我们观察数字 12，能整除它的 2 的最大幂次是 4，而能整除它的 3 的最大幂次是 3。这种工具通常被称为布奇谓词（Büchi predicate），它允许我们在不完全引入乘法的情况下讨论数字的幂。几十年来，核心问题在于，当我们尝试同时使用两个这样的工具时——特别是对于两个不具有简单乘法关系的基数时——会发生什么。如果我们试图同时使用两个不同基数的幂来描述数字，这个系统是保持可解性，还是会坍塌进入全乘法那种不可解的混沌之中？

牛津大学的研究员乔里斯·纽维尔德（Joris Nieuwveld）现在为这个问题的一个特定且重要的情形提供了明确的答案。该研究关注的是两个互质的基数，即除了 1 以外没有共同因子的基数，例如 2 和 3。虽然之前的研究表明，使用两个这样的基数通常会使系统变得不可判定，但纽维尔德证明，如果我们把问题限制在一种特定的、更简单的形式上——即只询问是否存在解，而不要求对所有可能的解进行完整描述——那么该系统仍然是可解的。论文证明了对于这些互质的基数，存在一种可靠的方法来确定一个给定的陈述是真是假，从而有效地驯服了一个此前被认为在此特定配置下难以处理的问题。

通往这一发现的道路需要穿越指数增长和模约束的景观。研究人员首先将复杂的逻辑问题转化为一个涉及两个基数的幂的包含不等式和模方程的系统。想象一下，这些幂可以作为变量进行极大的增长，而这些方程则是规定它们如何相互关联的规则。挑战在于，是否存在任何这些数字的组合能够同时满足所有的规则。该方法涉及将问题分解为可管理的层级，根据变量的大小关系对它们进行分组。通过分析这些层级的结构，研究人员可以识别出哪些变量是紧密结合在一起的，而哪些可以独立变化。

解决方案的一个关键部分依赖于对数字在被其他数的幂整除时行为的深刻理解。论文利用数论中一个强大的定理来表明，在某些条件下，这些幂的余数遵循可预测的模式。这种可预测性使得研究人员能够显著简化问题。该方法不再尝试求解每一个可能的数字，而是将无限的可能性减少为一组可以检查的有限情况。证明表明，如果基数是互质的，那么它们幂次的相互作用受到足够的约束，从而防止系统变得过于混乱而无法解决。

这一结果澄清了算术可判定性的边界。它证实了虽然添加两个布奇谓词通常会导致一个不可解的系统，但在互质基数的情况下，存在片段（即仅询问解的存在性的部分）仍然是可判定的。这一发现解决了一个关于此特定情况的长期悬而未决的问题。论文并未声称已经解决了所有可能的基数对的问题，特别是对于那些不互质的情况，那里的余数行为会变得更加不稳定，且当前的方法并不适用。然而，对于互质的情况，这项工作提供了一个完整且严谨的证明，证明存在决策程序。

这项工作之所以重要，是因为它完善了我们对“可计算”与“不可计算”之间界限的理解。在逻辑学和计算机科学的更广泛领域中，了解什么是可判定的极限对于设计验证软件、检查数学证明以及模拟复杂过程的系统至关重要。通过展示在特定条件下，一种自然扩展的算术系统仍然是可解的，这篇论文为数学逻辑的拼图添加了一个精确的碎片。它表明，即使在那些看似即将变得过于复杂而难以处理的系统中，只要我们使用正确的工具并保持适当的限制，仍然存在可以被绘制和理解的秩序之岛。

技术摘要：关于两个互质基数下的存在量词 Büchi 算术

问题陈述
本文研究了在带有序关系、加法和两个 Büchi 谓词的整数一阶逻辑存在量词片段 $\exists\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$ 的可判定性。这里， $V_z(x, y)$ 当且仅当 $y$ 是能整除 $x$ 的 $z$ 的最大幂次时成立。

背景由 Villemaire (1992) 建立，他证明了当 $\alpha$ 和 $\beta$ 为乘法独立时，全一阶理论 $\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$ 是不可判定的，因为该结构可以编码乘法。随后的研究由 Hieronymi 和 Schulz (2021) 开展，他们表明将 Büchi 谓词替换为较弱的幂谓词 ( $\alpha^\mathbb{N}, \beta^\mathbb{N}$ ) 也会导致理论不可判定。然而，Karimov 等人 (2025) 证明了对于乘法独立的基数，带有幂谓词的理论的存在量词片段是可判定的。

本文解决的开放问题是：当谓词是更强的 Büchi 谓词 ( $V_\alpha, V_\beta$ ) 而非简单的幂集时，存在量词片段是否仍然可判定。作者针对基数 $\alpha$ 和 $\beta$ 为互质的情况解决了这一问题。

方法论
证明过程通过一个量词消去论证进行，该论证将一个存在量词公式转化为一个涉及 $\alpha$ 和 $\beta$ 的幂次的线性不等式组和模约束系统。该方法依赖于几个关键的数学工具和结构化约简：

约简为不等式系统：
作者首先将存在量词公式约简为一个涉及“纯幂变量” ( $z^n$ ) 和“线性幂变量” ( $x \cdot z^n$ ) 的系统。该系统由线性不等式 ( $Ax > v$ ) 和模约束组成，其中包含常数模数以及具有变量模数的模数（形式为 $d \cdot z^n$ ）。
结构分解（层级与底层族）：
为了管理变量的复杂度，作者根据变量的相对大小将其划分为不同的“层级”（levels）。同一层级的变量其比例受常数限制，而不同层级的变量其比例可以任意大。
- 层级 (Levels)： 通过多面体 $Ax > v$ 的渐近锥进行定义。
- 底层族 (Bottom Family)： 一组特定的变量（特别是那些具有“小系数”的变量）被作为一个整体处理。作者定义了一个“底层族”，使得多面体在这些变量上的投影不是“薄”的（即在特定的线性方向上不是有界的）。
迭代约简与标准化：
算法的核心在于将系统约简为满足特定属性列表（属性 1–4c）的状态。这些属性确保了：
- 变量严格有序 ( $x_1 > \dots > x_t > 0$ )。
- 多面体不是薄的。
- 具有变量模数的模约束被处理，使得模数的基数不在底层族中。
- 各层级的正交子空间关于指数基数满足特定的非退化条件。
实现这些属性涉及应用 Baker 定理（关于对数线性形式）来限制指数，以及 Kronecker 定理（关于丢番图逼近）来确保比例的稠密性。
处理模约束：
一个关键的技术贡献是处理具有变量模数的模约束 ( $x \equiv c \pmod{z^n}$ )。作者利用了基于 $\alpha$ 和 $\beta$ 互质性的 引理 33。该引理指出，对于足够大的 $m$ ，集合 $\{\beta^n \pmod{\alpha^m}\}$ 的残余结构是稳定的。这使得作者能够“放大”指数，从而有效地通过缩放变量，将变量模数约束转换为常数模数约束（或具有固定周期性的约束）。
量词消去：
一旦系统被标准化且模数被固定（或约简为常数情况），作者应用一个提升论证。他们证明，如果系统是可满足的，则存在一个解，其中底层族之外的变量足够大。剩余的变量（在底层族中的变量）被视为特定模类内的线性整数。通过消除这些线性变量，系统被约减为规模更小的变量集，最终导致无量词决策。

主要贡献与结果

主定理： 本文证明了对于互质整数 $\alpha, \beta \ge 2$ ，存在量词片段 $\exists\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$ 是可判定的。
对前人工作的推广： 这一结果将 Karimov 等人的可判定性结果（适用于幂谓词 $\alpha^\mathbb{N}, \beta^\mathbb{N}$ ）推广到了更具表达能力的 Büchi 谓词 $V_\alpha, V_\beta$ ，并施加了互质这一更强的条件。
技术引理： 本文提供了特定的引理（例如引理 33），描述了互质基数的幂模幂的结构，这对于约简变量模数约束至关重要。
算法构建： 证明是构造性的，提供了一种计算必要的界限、划分和代换以消除量词的方法。

意义与局限性
本文声称解决了 Villemaire 原创扩张中对于互质基数的存在量词部分的判定问题。作者明确指出，对互质性的依赖是一个显著的约束。

对互质性的依赖： 证明中两次使用了互质性：一次是在应用 Baker 定理（引理 12）时，另一次更关键地是在关于 $\beta^n \pmod{\alpha^m}$ 结构的引理 33 中。作者指出，对于非互质但乘法独立的基数，残余集合的行为更加不规则（呈线性增长而非趋于稳定），作者尚不知道如何规避这一问题。
范围： 该结果仅针对存在量词片段。全理论仍然是不可判定的。
未来方向： 作者讨论了将此扩展到多个谓词（例如三个幂谓词）的情况，这可能需要使用 Schanuel 猜想来处理对数线性无关性。他们还指出，对于一般的乘法独立（非互质）基数的问题仍然是一个开放问题，可能需要新的思路，例如涉及 $p$ 进版本的 Baker 定理。

总而言之，本文确立了存在量词 Büchi 算术的可判定性边界，弥补了幂谓词与全 Büchi 谓词之间的差距，但也明确承认，对于一般的乘法独立基数，该问题仍然是一个挑战。

技术摘要：关于两个互质基数下的存在量词 Büchi 算术

类似论文