On the Decidability of Monadic Theories of Arithmetic Predicates

この論文「On the Decidability of Monadic Theories of Arithmetic Predicates（算術述語の単一述語論理の決定可能性について）」は、自然数上の順序関係と特定の算術述語（集合）を組み合わせた構造の、単一述語第二階論理（MSO）の決定可能性を研究したものです。

以下に、問題設定、手法、主要な貢献、結果、および意義について詳細な技術的サマリーを記述します。

1. 問題設定

本研究の対象は、構造 $\langle \mathbb{N}; <, P_1, \dots, P_d \rangle$ の MSO 理論の決定可能性です。ここで、$P_i \subseteq \mathbb{N}$ は自然数の部分集合（単一述語）であり、特に線形漸化式（LRS: Linear Recurrence Sequences）から生じる「算術的述語」に焦点を当てています。

具体的には、以下の 2 つの主要なケースを扱います。

1. 単一の非重複支配根を持つ整数線形漸化式の値集合:
   • 例: 固定底のべき乗 $k^\mathbb{N} = \{k^n : n \in \mathbb{N}\}$、$k$ 乗数 $\mathbb{N}^k = \{n^k : n \in \mathbb{N}\}$、フィボナッチ数列の項の集合など。
   • 一般的に、$P_i = \{a_i \rho_i^n : n \in \mathbb{N}\}$ のような形（幾何級数）や、より一般的な LRS の値集合。
2. べき乗とべき乗の混合:
   • 例: $P_1 = \{q n^d : n \in \mathbb{N}\}$（$d$ 乗数）と $P_2 = \{p b^n : n \in \mathbb{N}\}$（$b$ 底のべき乗）の組み合わせ。

既存の研究（Elgot-Rabin などの「縮約法」）は単一の述語に対する決定可能性を示してきましたが、複数の述語が相互作用する場合、その決定可能性は長年の未解決問題でした。特に、異なる底のべき乗（例: $2^\mathbb{N}$ と $3^\mathbb{N}$）や、べき乗と多項式（例: $2^\mathbb{N}$ と $\mathbb{N}^2$）の組み合わせにおける MSO 理論の決定可能性は不明でした。

2. 手法とアプローチ

著者らは、論理学、自動機理論、数論、および力学系理論を統合した新しいアプローチを採用しています。

1. 特徴語から順序語への縮約:

   • 述語 $P_1, \dots, P_d$ の特性を表す無限語（特徴語 $\alpha$）を、述語の要素が現れる順序のみを記録した「順序語（Order Word, $\beta$）」に圧縮します。
   • 述語が「効果的に周期的（effectively procyclic）」かつ「効果的に疎（effectively sparse）」である場合、特徴語 $\alpha$ の自動機受理問題と順序語 $\beta$ の自動機受理問題はチューリング同値であることが示されます（定理 3.12）。これにより、MSO 論理式 $\varphi$ の真偽判定が、順序語 $\beta$ に対する自動機の受理判定問題（$Acc_\beta$）に帰着されます。

2. 力学系理論の活用:

   • 順序語 $\beta$ の構造は、力学系の軌道としてモデル化できます。
   • ケース 1（LRS の支配根）: 順序語は、$d$ 次元トーラス $\mathbb{T}^d$ 上の並進（translation）$x \mapsto x + t$ によって生成される「切断列（cutting sequences）」または「ビリヤード語」として記述されます。クラメルの定理（Kronecker's theorem）や、線形独立な対数条件を用いて、この軌道が均一に再帰的（uniformly recurrent）であることを示し、決定可能性を導きます。
   • ケース 2（べき乗と多項式）: 順序語は、$x \mapsto \{b \cdot x\}$ によって生成される $b$ 進展開（base-$b$ expansion）に関連付けられます。これにより、MSO 理論が特定の代数数の $b$ 進展開の MSO 理論とチューリング同値であることが示されます。

3. 数論的仮定の利用:

   • 決定性の証明において、Schanuel の予想（超越数論の未解決予想）を仮定することで、対数の線形独立性条件を緩和し、より一般的なケース（例: $2^\mathbb{N}, 3^\mathbb{N}, 5^\mathbb{N}$）の決定可能性を条件付きで証明しています。
   • 条件付きアルゴリズムは、Schanuel の予想を「停止性」のみに依存し、「正しさ」については無条件に保証されるように設計されています。

3. 主要な結果と貢献

論文は、以下の具体的な決定可能性結果を導出しています。

• 無条件の決定可能性:

  • $\langle \mathbb{N}; <, 2^\mathbb{N}, \text{Fib} \rangle$ の MSO 理論は決定可能。
  • $\langle \mathbb{N}; <, 2^\mathbb{N}, 3^\mathbb{N}, 6^\mathbb{N} \rangle$ の MSO 理論は決定可能。
  • $\langle \mathbb{N}; <, 4^\mathbb{N}, \mathbb{N}^2 \rangle$ の MSO 理論は決定可能。
  • 一般に、$\log(\rho_1), \dots, \log(\rho_d)$ の対数が有理数体上で線形独立である場合、$\langle \mathbb{N}; <, a_1 \rho_1^\mathbb{N}, \dots, a_d \rho_d^\mathbb{N} \rangle$ の MSO 理論は決定可能（定理 4.4）。

• 条件付きの決定可能性（Schanuel の予想を仮定）:

  • 対数の線形独立性条件を緩和し、$\langle \mathbb{N}; <, 2^\mathbb{N}, 3^\mathbb{N}, 5^\mathbb{N} \rangle$ のようなケースを含む、より一般的なべき乗集合の MSO 理論が決定可能であることを示す（定理 4.6）。
  • Schanuel の予想は、対数間のすべての多項式関係を記述するため、これにより任意の $a_i, \rho_i$ に対する MSO 理論の決定可能性（非一意的なアルゴリズムとして）が保証されます（定理 4.9）。

• 代数数展開との同値性:

  • $\langle \mathbb{N}; <, 2^\mathbb{N}, \mathbb{N}^2 \rangle$ の MSO 理論は、$\sqrt{2}-1$ の 2 進展開 $\gamma$ を用いた構造 $\langle \mathbb{N}; <, \gamma \rangle$ の MSO 理論とチューリング同値です（定理 5.1, 5.3）。
  • $\sqrt{2}$ が正規数（normal number）であるという広く信じられている予想が真であれば、$\langle \mathbb{N}; <, 2^\mathbb{N}, \mathbb{N}^2 \rangle$ の MSO 理論は決定可能となります。

4. 意義とインパクト

• 論理学と力学系の融合: 従来の自動機理論や論理的手法だけでは扱えなかった、複数の算術述語の複雑な相互作用を、力学系（トーラス上の並進や $b$ 進展開）の観点からモデル化し、決定可能性を証明した点に大きな革新性があります。
• 未解決問題との関係: 本研究は、LRS の符号パターン（Sign Pattern）の決定可能性や、スキロム問題（Skolem Problem）などの未解決問題と密接に関連しています。特に、対角化可能な LRS の符号パターンの MSO 理論が決定可能であること（ただし、特定の多項式関係の計算が必要）を示唆しています。
• 数論的予想との接点: 決定可能性の証明が、Schanuel の予想や代数数の正規性予想といった深遠な数論的予想と結びついていることを明確にしました。これにより、論理の決定可能性問題が数論の未解決問題の解決を促す可能性を示しています。
• 実用的なアルゴリズムの枠組み: 特定の条件下（例: 底が $k^d$ の関係にある場合）では、完全に決定可能なアルゴリズムを提供しており、実際のモデル検査や形式検証への応用可能性を示唆しています。

結論

この論文は、算術的述語を含む自然数構造の MSO 理論の決定可能性に関する長年の課題に対し、力学系理論と数論を駆使した画期的な解決策を提示しました。特に、複数のべき乗やべき乗と多項式の組み合わせに対する新しい決定可能性結果は、論理学、計算理論、数論の境界領域における重要な進展です。