On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic

技術的概要：プレッスバー算術の可変有界非線形拡張について

問題定義
プレッスバー算術（整数の加法と順序に関する一階理論）は決定可能である。しかし、完全平方数の集合（$Z^2$）や一般の多項式像などの非線形述語による拡張は、一般の場合において決定不可能であることが知られている。この決定不可能性は、これらの理論内で乗法を符号化できることに起因する。このような拡張の存在論的フラグメントの決定可能性は依然として主要な未解決問題である（例えば、完全平方数に関するブッチの予想）が、本論文は決定可能性を回復するための別の道筋、すなわち変数の数を制限することに焦点を当てて調査を行う。

著者らは、単項多項式述語の族によるプレッスバー算術の変数有界拡張に焦点を当てる。具体的には、異なる変数の数が定数 $k$ によって制限されるフラグメント（$FO_k$、$\exists FO_k$、および $SMT_k$ と表記）を検討する。中心的な課題は、単一変数（$k=1$）の場合であっても、2 つの多項式述語が交差するかどうか（例えば、$f(u) = g(v)$）の決定可能性は、一般的に未解決であるヒルベルトの第 10 問題の極めて制限されたインスタンスである点にある。

手法
本論文は、数論的、代数幾何学的、および測度論的な手法を組み合わせ、これらの変数有界フラグメント内の制約の解集合を分析する。

1. 前処理と簡約: 決定手続きは、任意の文を、制約の論理積に関する充足可能性問題に簡約することから始まる。これらの制約には、線形不等式（$x > c$）、モジュラ算術（$x \equiv_m c$）、および $R(ax+b)$またはその否定$\neg R(ax+b)$ の形式の多項式述語が含まれる。著者らは中国剰余定理を利用してモジュラ制約を統合し、有界区間を排除するための場合分けを行い、問題を非有界領域における制約の充足可能性の決定に帰着させる。
2. 正の制約の処理: 手法の中核は、正の多項式制約のシステムの解集合を特徴づけることにある。
   • 固定されたべき乗（例：$Z_k = \{n^k\}$）の場合、著者らは超楕円ディオファントス方程式に関する結果を活用する。これら 2 つの制約の交わりは、次数が十分に高い場合は有限集合となり、次数が 2 の場合は線形漸化式（LRS）によってパラメータ化される集合となることが示される。
   • 次数が最大 3 の一般多項式の場合、分析は結果として生じる代数曲線の種数に依存する。3 次多項式を含むシステムは、しばしば種数 1（楕円曲線）またはそれ以上の曲線をもたらすが、シエーゲルの定理またはベイカーの境界により、これらは有限個の整数点しか持たない。2 次多項式を含むシステムはペル方程式に関連し、その解は可逆的な LRS を形成する。
3. 負の制約の処理（密度論証）: 重要な洞察として、正の制約に対する解集合が無限である場合、負の制約に違反する解の集合（すなわち、否定された述語の正のバージョンを満たす集合）は、元の解集合内において相対密度ゼロであるという点がある。
   • 多項式像の場合、像の成長率は多項式的であるのに対し、「禁止された」集合（異なる多項式に起因する場合）は、しばしば異なる速度で成長するか、まばらである。
   • 解集合が LRS である場合、著者らは「禁止された」解のインデックスが等差数列を形成することを証明する。これにより、密度ゼロの部分集合を除外した後に解が残存するかどうかを判定するための実効的なチェックが可能となる。
4. 冗長性と統合: 著者らは「冗長」および「類似」の制約の概念を定義する。冗長な制約は破棄でき、類似した制約は $p$ 進付値と中国剰余定理を用いて単一の制約に統合でき、密度論証を適用する前にシステムを簡素化する。

主要な貢献と結果

本論文は、単一変数理論（$k=1$）に対して 2 つの主要な決定可能性結果を確立する。

1. 固定されたべき乗による決定可能性: 理論 $FO_1\langle \mathbb{Z}; 0, 1, +, -, <, (\equiv_m)_{m\ge 2}, (Z_k)_{k\ge 2} \rangle$ は決定可能である。この結果は、超楕円ディオファントス方程式（$w^k - nz^j = N$）の可解性と、そのような方程式のシステムが有限個の解または LRS によってパラメータ化される解を持つという事実に依存している。
2. 低次数多項式による決定可能性: 理論 $FO_1\langle \mathbb{Z}; 0, 1, +, -, <, (\equiv_m)_{m\ge 2}, (R_i)_i \rangle$ は決定可能である。ここで、各 $R_i$ は次数が最大 3 の整数値多項式の像に対応する。この結果は、関連する代数曲線の低い種数（種数 0 または 1）と、同時ペル方程式の解の構造を利用している。

決定不可能性の結果
これらの肯定的な結果の境界を明確にするため、本論文は変数制限を解除した場合や特定の述語が組み合わされた場合の決定不可能性の証明を提供する。

• 存在論的フラグメント $SMT_2\langle \mathbb{Z}; 0, 1, +, -, Z^2 \rangle$ は決定不可能である。これは、ブッチの予想の否定を符号化することによって示され、これにより限られた数の変数を用いて乗法の定義が可能となる。
• ジョーンズの普遍的ディオファントス方程式と、ブッチの予想に関するシャオの最近の証明を用いて、著者らは、変数数が著しく多い理論（例えば、$Z^2$ を含む $SMT_{600}$ または $SMT_{2200}$）が決定不可能であることを確立する。

意義
本論文の意義は、プレッスバー算術の非線形拡張において、決定可能性が回復し得る正確な境界を特定することにある。変数の数を 1 つに制限することで、著者らは、ディオファントス幾何学の深い結果（種数 $\ge 2$ の曲線上の整数点の有限性など）および線形漸化式理論が、決定手続きを構築するのに十分であることを実証している。

この研究は二項対立を浮き彫りにする。すなわち、一般的な非線形拡張は決定不可能であり、2 変数と完全平方数による存在論的フラグメントさえも決定不可能である一方で、単一変数のケースは広範な述語の族に対して扱い可能であるという点である。著者らは、これらの結果を 2 変数または 3 変数に拡張することは、3 変数と $Z^2$ を必要とする完全なオイラーのレンガの存在や、2 変数と $Z^3$ を必要とする 3 乗和の問題といった有名な未解決問題によって阻害されると指摘している。したがって、本論文は、変数制限によって制約された算術理論の計算複雑性を理解するための厳密な枠組みを提供する。