Undefinability of multiplication in Presburger arithmetic with sets of powers
我们首先证明，任何Presburger定义的一组或多组权力的形象有零自然密度。然后，通过修改Friedman和Miller关于o-极小结构的一个二分法结果的证明，我们得到了关于整数上Presburger算术展开式的一个类似的二分法。结合这两个结果，我们得到整数的序群被任意个数的幂集展开并不定义乘法。
2022-09-23 math.LO
Multi-Dimensional Interpretations of Presburger Arithmetic in Itself
Presburger算术是自然数的加法运算的真正理论。我们研究普雷斯堡算术本身的解释。本文的主要结果是，所有的自我解释是可定义同构的平凡。在这里，我们考虑可能是多维的解释。我们注意到这解决了A的一个猜想。维瑟为了证明这个结果，我们证明了所有的线性序是解释在$(\mathbb{N};+)$是分散的顺序与有限的Hausdorff秩和秩有界的维度的各个解释。
2020-04-05 math.LO
There are no intermediate structures between the group of integers and Presburger arithmetic
我们证明了如果一个一阶结构$\mathcal{M}$，其论域为$\mathbb{Z}$，是$(\mathbb{Z},+,0)$的展开和$(\mathbb{Z},+,<,0)$的约化，则$\mathcal{M}$必须与$(\mathbb{Z},+,0)$或$(\mathbb{Z},+,<,0)$互定义.
2018-07-13 math.LO
Rigid models of Presburger arithmetic
我们提出了一个描述的刚性模型的Presburger算法（即，Z-基团）。特别是，我们表明，Presburger算法具有刚性模型的所有无限基数的连续，但没有更大的。
2018-11-08 cs.LO math.LO
Speedups for Presburger Arithmetic and Real Closed Fields
本文通过比较两种公理化方法的证明长度，展示了Presburger算术和实闭域理论在公理化上的双指数速度提升。
2026-02-28 math.LO
Decidability of extensions of Presburger arithmetic by generalised polynomials
本文证明了特定形式的二次广义多项式扩展Presburger算术导致不可判定性。
2025-10-01 math.LO math.NT
Uniform definition of sets using relations and complement of Presburger Arithmetic
1996年，Michaux和Villemaire考虑了在Presburger算术中不可定义的整数关系$R$。也就是说，在一阶逻辑中，对于具有加法函数和顺序关系（FO[N，+，<]-可定义关系）的整数是不可定义的。他们证明了，对于每个这样的$R$，存在一个FO[N，+，<，$R$ ]-公式$ν_{R}(x)$，它定义了一组整数，这些整数不是最终周期的，即不是FO[N，+，<]-可定义的。本文证明了可以选择公式$ν(x)$，使得它不依赖于对$R$的解释。进一步证明了可以选择$ν(x)$使得它定义一个扩展集。也就是说，整数的无限集使得两个连续元素之间的距离没有界限。
2016-11-11 math.LO
Fibonacci Numbers and Model-Complete Axiomatization of Presburger Arithmetic Expanded with a Beatty Sequence
引入递归理论完全公理化包含Beatty序列的Presburger算术结构，并证明在扩展Fibonacci floor函数的语言中该公理化是模型完备的。
2025-09-17 math.LO
Decidability bounds for Presburger arithmetic extended by sine
我们考虑Presburger算法的正弦函数扩展，称之为正弦Presburger算法（$\sin$ -PA），并系统地研究了决策问题的$\sin$ -PA的句子集。特别地，在Schanuel猜想的假设下，给出了一个存在$\sin$ -PA语句的判定算法.这个过程减少决策的理论有序添加剂群的实数扩展正弦，这是决定下Schanuel猜想。另一方面，我们证明了四个交替的量词块足以满足$\sin$ -PA句子的不可判定性。要做到这一点，我们明确解释弱一元二阶理论的网格，这是不可判定的，在$\sin$ -PA。
2022-05-02 cs.LO math.LO
Distal expansions of Presburger arithmetic by a sparse predicate
该研究证明由同余周期稀疏谓词扩张的Presburger算术结构具有远端性，通过构造强诚实定义实现证明，为具体远端分解提供了罕见实例。
2024-10-10 math.LO math.NT
A Dichotomy for $k$-automatic expansions of Presburger Arithmetic
University of Waterloo（滑铁卢大学）；Universiteit van Amsterdam（阿姆斯特丹大学）
研究$ k $-自动集在Presburger算术扩展中的定义性，证明要么所有$ k $-自动集可定义，要么$(\mathbb{N},+,X)$与$(\mathbb{N},+,k^{\mathbb{N}})$定义集相同。
2026-05-13 cs.FL math.LO
Axiomatizations of Presburger Arithmetic With Predicates For Powers
University of Bonn（波恩大学）；University of Manchester（曼彻斯特大学）
该研究为带有幂函数谓词的Presburger算术提供了公理化，并证明了其可判定性。
2026-02-23 math.LO
Complexity of short Presburger arithmetic
研究了Presburger算法中短句的复杂性。这里的“短”是指包含有限数量的变量、量词、不等式和布尔运算的句子;输入仅由不等式中涉及的整数组成。我们证明了，假设Kannan的划分可以在多项式时间内找到，短PA句子的可满足性可以在多项式时间内决定。此外，在同样的假设下，我们证明了短Presburger句子的满意分配的数量也可以在多项式时间内计算。
2017-04-28 cs.CC cs.DM cs.LO
Stable reducts of elementary extensions of Presburger arithmetic
本文证明，与具有小商群的阿基米德有序阿贝尔群初等等价的结构，其扩张了加法群的稳定归约必与加法群相互可定义，推广了先前关于整数加法群的结果，并回答了 Conant 2018 年的问题。
2025-04-20 math.LO
Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior
参数Presburger算术涉及集合S_t在Z^d中的族，其中t在N中，这些集合是使用加法、不等式、Z中的常数、布尔运算、乘以t和变量范围在Z上的量词来定义的。也就是说，这样的族是使用量词和形式为a（t）x <= b（t）的公式的布尔组合来定义的，其中a（t）在Z[t]^d中，b（t）在Z[t]中。函数g：N -> Z是拟多项式，如果存在周期m和多项式f_0，.，f_{m-1}在Q[t]中，使得g（t）=f_i（t），其中t全等于i（mod m.）Chen、Li、Sam的最新结果; Calegari、Walker; Roune、Woods;和Shen关注参数Presburger算术中表现出准多项式行为的特定族。例如，S_t可能是t的准多项式函数，或者S_t中的元素x（t）可以指定为具有准多项式坐标的函数，对于足够大的t。伍兹指出，所有参数Presburger集都表现出这种准多项式行为。在这里，我们证明这个猜想，使用各种工具，从逻辑和组合。
2017-01-16 math.CO math.LO
Periodic behavior in families of numerical and affine semigroups via parametric Presburger arithmetic
设$f_1(n), \ldots, f_k(n)$是$n$的多项式函数。对于固定的$n\in\mathbb{N}$，设$S_n\subseteq \mathbb{N}$是由$f_1(n),\ldots,f_k(n)$生成的数值半群。随着$n$的变化，我们证明了$S_n$的许多不变量最终在$n$中是拟多项式的，如Frobenius数、类型、亏格和$Δ$ -集的大小.我们使用的工具是参数Presburger算法逻辑系统的可表达性。推广到高维半群族，我们还研究了由其坐标是$n$的多项式函数的向量生成的仿射半群$S_n\subseteq \mathbb{N}^m$，并且我们证明了类似的结果，例如，贝蒂数最终是$n$的拟多项式函数。
2019-11-20 math.CO math.LO
Short Presburger arithmetic is hard
研究了Presburger算法（Short-PA）中短句的计算复杂性。这里的“短”是指具有有限数量的变量、量词、不等式和布尔运算的句子;输入仅由线性不等式中涉及的整数系数组成。证明了当第一个量词为$\exists$或$\forall$时，含有$m+2$交替量词的短PA句的可满足性分别是$Σ_{P}^m$ -完全或$Π_{P}^m$ -完全的.对计数版本和受限系统也进行了分析。进一步应用于随机优化中两个自然问题的困难性。
2017-10-20 cs.CC cs.LO math.CO
Presburger arithmetic, rational generating functions, and quasi-polynomials
Presburger算术是自然数加（但不乘法）的一阶理论。我们刻画了可由Presburger公式定义的集合为其特征函数可由有理生成函数表示的集合，并给出了这类集合的几何刻画.此外，如果p=（p_1，...，p_n）是Presburger公式中自由变元的子集，我们可以定义一个计数函数g（p）为该公式的解的个数，对于给定的p，我们证明了这样得到的每一个计数函数都可以等价地表示为分段拟多项式或有理母函数.最后，我们将已知的计算复杂性结果转化为这种设置，并讨论开放的方向。
2015-01-06 cs.LO math.CO math.LO
Decidability of Extensions of Presburger Arithmetic by Hardy Field Functions
研究Presburger算术通过次多项式Hardy域函数的扩展，证明当函数f增长快于x或次线性但不慢于某多项式时，带最近整数算子的扩展理论Th(ℤ; <, +, ⌊f⌉)不可判定。
2025-08-26 cs.LO math.LO math.NT
An efficient quantifier elimination procedure for Presburger arithmetic
本文提出一种可在单指数时间内消去存在量词变量块的Presburger算术量词消去过程，纠正了双重指数时间上界为紧的旧有论断，并据此确定了单元可分解性、良拟序判定及Ramsey量词公式等问题的精确复杂度。
2024-05-02 cs.FL cs.LO math.LO
VC-dimension of short Presburger formulas
研究了Presburger算术中短公式的VC-维数，定义为变量、量词和原子的个数有界。我们给出了下限和上界，这是紧到一个多项式因子的位长度的公式。
2017-10-11 cs.LO math.CO math.LO
Some properties of Büchi Arithmetics
本文研究Büchi算术的性质，证明其可解释任意大有限秩的线性序，且用$V_n$的归纳定义扩展Presburger算理公理无法构成其公理化。
2023-10-24 math.LO
Parametric Presburger Arithmetic: Complexity of Counting and Quantifier Elimination
我们考虑一个扩展的Presburger算法，它允许乘以$k$参数$t_1,\ldots,t_k$。该语言中的公式定义了参数集$S_\mathbf{t} \subseteq \mathbb{Z}^{d}$，因为$\mathbf{t}$在$\mathbb{Z}^k$中变化，并且我们将计数函数$|S_\mathbf{t}|$作为$\mathbf{t}$的函数进行检查。对于单个参数，已知$|S_t|$可以表示为最终的准多项式（存在周期$m$，使得对于足够大的$t$，函数在每个剩余类mod $m$上是多项式）。我们表明，这样一个很好的表达式是不可能有2个或更多的参数。实际上（假设\textbf{P} $\neq$ \textbf{NP}），我们构造参数集$S_{t_1,t_2}$，使得$|S_{t_1, t_2}|$甚至不能在输入$(t_1,t_2)$上多项式时间计算。与此相反，参数集$S_\mathbf{t} \subseteq \mathbb{Z}^d$任意多个参数，定义在一个类似的语言没有顺序关系，我们表明，$|S_\mathbf{t}|$总是多项式时间计算的大小$\mathbf{t}$，事实上可以表示使用的gcd和类似的功能。
2018-02-03 cs.CC math.CO math.LO
Presburger Arithmetic with algebraic scalar multiplications
该研究将Presburger算术扩展为带代数无理数标量乘法的α-PA，证明其判定复杂度远超PA：二次α时需塔式空间且特定量词结构为PSPACE-hard，非二次α时四块量词即不可判定。
2021-07-19 cs.CC cs.LO math.CO
On Interpretations in Büchi Arithmetics
Büchi算术BA_n，n ≥ 2，是Presburger算术的推广，其中一元函数符号V_n（x）表示n的最大幂除x。BA_n中的集合的可定义性等价于它被一个有限自动机以其n元展开接收数的可识别性。我们证明了Büchi算术BA_n和BA_m对任意n，m都是双可解的.进一步证明了BA_n中某个结构的任何解释都同构于某个一维解释，但这个同构不一定是BA_n可定义的。
2022-11-29 math.LO
Decidability for Sturmian words
该研究证明Presburger算术上Sturmian字的一阶理论可判定，借助通用加法器论证其一致ω-自动性，并用Pecan算法实现复现经典定理、得到特征Sturmian字中反平方与反回文的新结果。
2024-08-02 cs.LO math.CO math.LO
On the first order theory of plactic monoids
本研究通过将plactic幺半群双向解释到Presburger算术中，证明有限秩plactic幺半群的一阶理论可判定，解决了相关可判定性问题，并正面回应了无限秩情形的丢番图问题可判定性。
2024-05-16 math.GR math.LO
A note on arithmetic in finite types
我们提出了一个版本的算术在所有有限型，它允许一个定义的平等在更高的类型，所有的同余是可推导的，其中的合理性的辩证法解释是证明内部的系统本身，这允许内涵和外延的模型和演绎定理。
2016-09-20 math.LO
The Berry-like Sentence in the First-order Peano Arithmetic System with the Operation of Factorial
介绍了一种带阶乘运算的一阶Peano算术系统（PAF）。对于PAF中任意一个含有自由变元x的公式A（x），定义了一个相应的B-公式，即当A（x）可满足时，在满足公式A（x）的所有自然数中，存在唯一的最小数满足B-公式.然后，我们构造了一个公式，表示“存在x，对于任何一个哥德尔码小于小于常数a的B-公式，x不满足这个B-公式，并且x是具有这种特征的数中最小的。“然而，构造的公式本身是一个B-公式，它的哥德尔码小于a。因此，这是一个版本的PAF贝里句子“最小的正整数不能命名的11个字以下”，本身只有10个字。
2006-07-19 math.LO
Weak essentially undecidable theories of hereditarily finite multisets
该研究引入遗传有限多重集的一阶理论WF⁻和F⁻，证明WF⁻与R、F⁻与Q相互可解释，F⁻本质不可判定。克服多重集恢复有序对障碍，展示顺序与多重性的关系，还证明公理独立性及应用于斯宾塞 - 布朗形式，定位本质不可判定边界。
2026-07-14 math.LO
Fixed Points of Self-embeddings of Models of Arithmetic
研究了算术模型自嵌入的不动点集的结构。特别地，给定Peano算术的一个适度片段的可数非标准模型M，我们给出了（a）M的初始段的完整刻画，这些初始段可以被实现为M到M的一个适当的初始段上的非平凡自嵌入的不动点的最长初始段;以及（b）M的初始段，它可以被实现为M的某个非平凡自嵌入到M的真初始段上的不动点集。此外，我们证明了标准割在M中是强的当且仅当M存在一个自嵌入到其自身的一个适当的初始段上，该自嵌入移动M中所有不可定义的元素。
2018-01-22 math.LO
A fixed point for the jump operator on structures
假设$0^#$存在，我们证明存在一个结构，可以有效地解释自己的跳跃。特别地，我们得到一个结构$\mathcal A$，使得\[ Sp({\mathcal A}) = \{{\bf x}':{\bf x}\in Sp ({\mathcal A})\}, \]，其中$Sp ({\mathcal A})$是计算$\mathcal A$的副本的图灵度的集合。事实证明，比结果本身更有趣的是它意想不到的复杂性。我们证明了高阶算术，这是所有$n$全$n$阶算术的联合，不能证明这样的结构的存在。
2011-06-05 math.LO
