两个互素基下的存在性Büchi算术
On existential Büchi arithmetic in two coprime bases
浏览论文内容
中文总结 AI 辅助
该研究解决了互素基下Presburger算术扩展Büchi谓词的存在片段的可判定性问题，通过量词消去论证证明其可判定。
中文摘要 AI 辅助
对于乘法独立的自然数α和β，Villemaire在1992年证明，Presburger算术同时扩展Büchi谓词V_α和V_β后的一阶理论是不可判定的，因为它编码了乘法。近年来，Hieronymi和Schulz证明，Presburger算术同时扩展较弱的幂谓词α^ℕ={α^n:n∈ℕ}和β^ℕ后的理论也不可判定，而Karimov等人证明该理论的存在片段是可判定的。这些结果留下一个自然问题：Villemaire最初扩展理论的存在片段的可判定性。我们针对互素的α和β解决了这个问题，具体而言，我们给出量词消去论证，证明FO(ℤ;<,+,V_α,V_β)的存在片段是可判定的。
英文摘要
For multiplicatively independent natural numbers $α$ and $β$, Villemaire showed in 1992 that the first-order theory of Presburger arithmetic expanded with both Büchi predicates $V_α$ and $V_β$ is undecidable, as it encodes multiplication. In recent years, Hieronymi and Schulz showed that Presburger arithmetic expanded with the weaker power predicates $α^\mathbb{N} = \{α^n: n \in \mathbb{N}\}$ and $β^\mathbb{N}$ is also undecidable, while Karimov et al. showed that the existential fragment of this theory is decidable. These results left open the natural problem of determining the decidability of the existential fragment of Villemaire's original expansion. We settle this question for coprime $α$ and $β$. Specifically, we give a quantifier-elimination argument that proves the decidability of the existential fragment of $\mathsf{FO}(\mathbb{Z};<,+, V_α, V_β)$.
