On existential Büchi arithmetic in two coprime bases

技術的要約：2つの互いに素な底における存在量化ブキ算術について

問題提起
本論文は、順序、加法、および2つのブキ述語（$\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) により、ブキ述語をより弱いべき集合（$\alpha^\mathbb{N}, \beta^\mathbb{N}$）に置き換えた場合でも、理論が決定不能になることが示された。しかし、Karimovら (2025) は、乗法的独立な底を持つべき集合を用いた場合の理論の存在量化断片は決定可能であることを示した。

本論文が取り組む未解決問題は、述語が単純なべき集合ではなく、より強力なブキ述礼（$V_\alpha, V_\beta$）である場合に、存在量化断片が依然として決定可能であるかどうかである。著者は、底 $\alpha$ と $\beta$ が互いに素である場合に限定して、この問いに決着をつける。

手法
証明は、存在量化式を、「純粋べき変数」（$z^n$）と「線形べき変数」（$x \cdot z^n$）を含む不等式系および剰余制約へと変換する、量化消去の議論を通じて進められる。その手法は、いくつかの主要な数学的ツールと構造的簡約に依存している：

1. 不等式系への簡約:
   著者はまず、存在量化式を、純粋べき変数（$z^n$）と線形べき変数（$x \cdot z^n$）を含む系へと簡約する。この系は、線形不等式（$Ax > v$）と、定数法（moduli）を持つもの、および可変法（moduli）を持つもの（$d \cdot z^n$ の形式）を持つ剰余制約から構成される。

2. 構造的分解（レベルとボトム・ファミリー）:
   変数の複雑さを管理するために、著者は変数の相対的な大きさに基づいてそれらを「レベル」に分割する。同じレベルにある変数は比率が定数で抑えられているが、異なるレベルにある変数は任意に大きな比率を持ち得る。

   • レベル: 多面体 $Ax > v$ の回帰錐（recession cone）を通じて定義される。
   • ボトム・ファミリー（Bottom Family）: 「小さな係数」を持つ特定の変数の集合であり、これらは一括して扱われる。著者は、多面体のこれらの変数への射影が「薄くない」（すなわち、特定の線形方向において有界ではない）ような「ボトム・ファミリー」を定義する。

3. 反復的簡約と正規化:
   アルゴリズムの中核は、システムを特定の性質のリスト（特性1–4c）を満たすように簡約することである。これらの特性は以下を保証する：

   • 変数が厳密に順序付けられていること（$x_1 > \dots > x_t > 0$）。
   • 多面体が薄くないこと。
   • 可変法を持つ剰余制約において、その法の底がボトム・ファミリーに含まれていないこと。
   • レベルの直交部分空間が、指数底に関する特定の非退化条件を満たしていること。

   これらの特性を実現するために、指数の値を抑えるためのベイカーの定理（対数の線形形式に関する定理）と、比率の稠密性を保証するためのクロネッカーの定理（ディオファントス近似に関する定理）を適用する。

4. 剰余制約の処理:
   可変法を持つ剰余制約（$x \equiv c \pmod{z^n}$）の処理は、極めて重要な技術的貢献である。著者は、$\alpha$ と $\beta$ の互いに素性に依拠した補題33を利用する。この補題は、剰余の集合 $\{\beta^n \pmod{\alpha^m}\}$ が、大きな $m$ に対して構造的に安定することを述べている。これにより、著者は指数を「膨らませる（blow up）」ことで、可変法制約を定数法制約（または固定された周期性を持つ制約）へと実質的に変換することができる。

5. 量化消去:
   システムが正規化され、法が固定（または定数のケースに減少）された後、著者は持ち上げ（lifting）の議論を適用する。もしシステムが充足可能であれば、ボトム・ファミリーの外側にある変数が十分に大きい解が存在することを示す。残りの変数（ボトム・ファミリー内の変数）は、特定の剰余類内における線形整数として扱われる。これらの線形変数を消去することで、システムはより小さな変数の集合へと縮小され、最終的に量化子を含まない決定へと至る。

主要な貢献と結果

• 主定理: 本論文は、互いに素な整数 $\alpha, \beta \ge 2$ に対して、存在量化断片 $\exists\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$ が決定可能であることを証明している。
• 先行研究の一般化: この結果は、べき述語（$\alpha^\mathbb{N}, \beta^\mathbb{N}$）に適用された Karimov らの決定可能性の結果を、より強い条件である互いに素性の下で、より表現力の高いブキ述語 $V_\alpha, V_\beta$ へと拡張するものである。
• 技術的補題: 論文は、可変法制約の簡約に不可欠な、互いに素な底のべき乗のべき乗の構造を記述する具体的な補題（例：補題33）を提供している。
• アルゴリズム的構成: 証明は構成的であり、境界、分割、および置換を計算する方法を提供している。

意義と限界
本論文は、互いに素な底の場合における Villemaire の元の拡張に対する、存在量化断片の決定可能性の問題に決着をつけた。著者は、互いに素であることへの依存が重要な制約であることを明示している。

• 互いに素性への依存: 著者は、ベイカーの定理（補題12）の適用と、$\beta^n \pmod{\alpha^m}$ の構造に関する補題33において、二度にわたり互いに素性を利用している。著者は、互いに素ではない乗法的独立な底の場合、剰余の集合は（安定するのではなく）線形に増大するなど、より不規則に振る舞うことを指摘しており、この問題を回避する方法を現時点では知らないとしている。
• 範囲: この結果は存在量化断片に特化したものである。完全な理論は依然として決定不能である。
• 今後の方向性: 著者は、より多くの述語（例えば3つのべき述語）への拡張には、対数の線形独立性を扱うためにシャニエルの予想が必要になるであろうと述べている。また、一般的な（互いに素ではない）乗法的独立な底に関する問題は未解決であり、おそらく $p$ 進版のベイカーの定理など、新しいアイデアを必要とするであろうとも指摘している。

要約すると、本論文は、べき述語と完全なブキ述語の間のギャップを埋めることで、存在量化ブキ算術の決定可能性の境界を確立したが、一般的な乗法的独立な底については、依然として未解決の課題であることを明示している。