Toward a Characterization of Simulation Between Arithmetic Theories

技術要約：算術理論間のシミュレーションの特性付けに向けて

問題提起
本論文は、証明複雑性における「特性付け問題（Characterization Problem）」に取り組んでいる。すなわち、健全な算術理論 $S$（$S \supseteq S^1_2$ であり、公理が多項式時間で決定可能であるとする）が、真であるが $S$ から独立した文 $\phi$ に対して、有界一貫性命題 $\text{Con}_{S+\phi}(n)$ を効率的に証明するかどうかを判定する問題である。ここで、$\text{Con}_{S+\phi}(n)$ は、$S+\phi$ が $n$ 個の記号以内で $0=1$ を証明しないことを主張する。

証明複雑性の観点からは、これは $S$ が（証明系として見たときに）$S+\phi$ をシミュレートしているかどうかを問うている。ここで以下の区別を行う：

• シミュレーション (Simulation): $S \vdash^{n^{O(1)}} \text{Con}_{S+\phi}(n)$。これは、有界一一貫性命題の族に対して、多項式サイズの $S$ の証明が存在することを意味する。
• 非シミュレーション／困難性 (Non-simulation/Hardness): すべての定数 $c$ に対して、$S \nvdash^{n^c} \text{Con}_{S+\phi}(n)$。これは、多項式サイズの証明が存在しないことを意味する。

中心的な課題は、シミュレーションが発生するかどうかを支配する $\phi$ の必要十分条件を特定することである。単なる独立性だけではシミュレーションを排除できない（一部の独立な $\phi$ は多項式時間での解釈を許容するため）。最適証明系の存在は未知であり、もし存在しないならば、非シミュレーションとなる $\phi$ が存在しなければならない。

手法と枠組み
本論文は、$S^1_2$ を拡張する健全な算術理論内で動作し、構文の標準的な算術化を利用する。また、以下の3つを区別する：

1. 外部的シミュレーション (External Simulation): 標準モデルにおける短い証明の存在。
2. 内部的証明 (Internal Certification): 基底理論 $B$（例：初等算術、EA）がそのような証明の存在を証明できるかどうか。
3. 相対的一貫性 (Relative Consistency): 弱い基底理論（例：EA）において定式化された含意 $\text{Con}_S \to \text{Con}_{S+\phi}$。

手法は以下に依拠する：

• 証明翻訳 (Proof Translation): 解釈を用いて理論間の証明を翻訳すること。
• ビジービーバー減少 (Busy Beaver Reductions): 正確なビジービーバー値（$\phi_{BB(k)}$）を、証明不可能な情報の標準的なソースとして利用すること。
• コルモゴロフ複雑性 (Kolmogorov Complexity): ランダムな公理（$x \in R$）を分析し、情報理論的な障害を孤立させること。

主要な貢献と結果

1. 特性付けに対する無条件の制約
本論文は、シミュレーションの特性付けを制約するいくつかの無条件の結果を確立している：

• シミュレーションの十分条件 (定理 3.4): 有限公理化された逐次理論 $S$ について、$\text{EA} \vdash \text{Con}_S \to \text{Con}_{S+\phi}$ ならば、$S$ は $S+\phi$ をシミュレートする。これは、弱い基底理論における相対的一貫性が、有界な相対的一貫性（多項式時間の証明翻訳）を意味することに依拠しており、Friedman–Visser の解釈可能性基準と証明翻訳に基づいている。
• ビジービーバー転送 (定理 3.10): もし、真の文 $\phi$ が存在して $S$ が $S+\phi$ をシミュレートできない場合、十分大きな $k$ に対して、$S$ は $S^1_2 + \phi_{BB(k)}$ もシミュレートできない。これは、非シミュレーションが存在する場合、それは弱すぎる基底の拡張である標準的なビジービーバー拡張によって証されることを示している。
• 拡張標準形 (補題 3.14): 一貫したターゲット理論 $T$ に対するあらゆる困難性は、$S + \text{Con}_T$ という一文の拡張に対する困難性として再符号化できる。
• 証明の障壁 (定理 6.3): 基底理論 $B$ が $S$ が $U$ をシミュレートすること（大きな $n$ に対して一様に）を証明する場合、$B \vdash \text{Con}_S \to \text{Con}_U$ となる。したがって、$B$ が相対的一貫性の含意を証明できない場合、そのシミュレーションを証明（認証）することはできない。これにより、EA が $\text{Con}_S$ による拡張、正確なビジービーバー的事実、またはほとんどのコルモゴロフ・ランダムな公理によるシミュレーションを証明できないという、無条件の結果が得られる。

2. 中心的な予想：高次相対的一貫性 (HRC)
（充足条件である定理 3.4 と、Pudlák の予想（$S$ は $S+\text{Con}_S$ をシミュレートしない）との間のギャップに着想を得て、本論文は 高次相対的一貫性 (Higher Relative Consistency, HRC) を特性付けとして提案する：

• HRC (予想 5.1): 健全で有限公理化された逐次理論 $S$ と真の文 $\phi$ について、$\text{EA} \nvdash \text{Con}_S \to \text{Con}_{S+\phi}$ ならば、任意の定数 $c$ に対して $S \nvdash^{n^c} \text{Con}_{S+\phi}(n)$ である。
• 実現可能反射への同値性 (Equivalence to Feasible Reflection, FR): HRC は、実現可能反射（Feasible Reflection）の対偶である。これは、「もし $S$ が $S+\phi$ をシミュレートするならば、$\text{EA} \vdash \text{Con}_S \to \text{Con}_{S+\phi}$ である」という命題の対偶である。
• 含意: HRC の下では、シミュレーションは「弱い基底が、$\phi$ を加えることが一貫性を保持することを証明できるとき」にのみ発生する。これにより、様々な困難性の現象が統一される：
  • Pudlák の予想: $\text{EA} \nvdash \text{Con}_S \to \text{Con}_{S+\text{Con}_S}$ であるため、直ちに導かれる。
  • コルモゴロフ困難性 (Kolmogorov Hardness, KH): ランダムな公理 $x \in R$ について、$\text{EA} \vdash \text{Con}_S \to \text{Con}_{S+(x \in R)}$ でない限り、シミュレーションは失敗する。Chaitin の不完全性定理によれば、これは有限個の $x$ に対してのみ成立するため、ほとんどのランダムな公理は困難な拡張をもたらす。
  • ビジービーバー困難性: 十分に大きな $k$ に対して、$\phi_{BB(k)}$ は、相対的一貫性が EA において可視的でない限り、非シミュレーションをもたらす。

3. 有限スケールおよびペアワイズ拡張
本論文は、困難性が単に漸近的なものではなく、一様な閾値を超えると指数関数的になることを示唆する、より強い有限スケールの予想（SETH-K-Finite）を検討している。さらに、「Pairwise SETH-K-Finite」を提案し、独立にランダムな公理は互いに助け合わない（$x$ と $y$ が相互に条件付きランダムである場合、$y \in R$ を加えることは $\text{Con}_{S+(x \in R)}(n)$ のための短い証明をもたらさない）と主張している。

4. 外部的シミュレーションと内部的証明の区別
技術的な重要な貢献は、外部的シミュレーション（標準モデルにおける真理性）と内部的証明（基底理論における証明可能性）の分離である。本論文は、実現可能反射に対する反例には、EA が証明できない外部的に真なシミュレーションが必要となるが、EA がシミュレーションを証明できないという事実自体は、必ずしもシミュレーションが外部的に失敗することを証明しないことを示している。この区別により、「証明の障壁」とは、弱すぎる基底が何を「証明できるか」の限界であり、必ずしも絶対的な証明長の低界ではないことが明確になる。

意義と主張
本論文は、特性付け問題を解決したり HRC を証明したりすることを目的としているのではない。むしろ、以下のことを主張している：

1. 制約の孤立: どのような成功した特性付けも満たすべき、無条件の構造的制約（ビジービーバー転送、証明の障壁）を特定した。
2. 構造的な全体像の提示: 弱い基底における相対的一貫性の失敗が、シミュレーションに対する正確な障害となるという、HRC を「自然な」組織原理として提示した。
3. 困難性の源泉の統一: カノニカルな証明不可能な情報の源（ビジービーバー値、コルモゴロフ・ランダム性）は、単に便利なエンコーディングではなく、構造的な障壁を反映していることを示した。すなわち、シミュレーションは、基底理論が公開された証明記述を通じて回収できない真の情報へのアクセスを必要とする場合に失敗する。
4. 景観の洗練: もし HRC が成立するならば、硬いトートロジーを見つける問題は、相対的一貫性の分類問題へと還元される。そこでは、「容易な」拡張とは、弱い基底による相対的一貫性によって説明されるものに限定され、それ以外はすべて「硬い」ものとなる。

本論文は、HRC を証明することが、相対的一貫性を完全な特性付けへと変える大きな進展となることを示唆しているが、そのためには計算複雑性理論の中心的な未解決問題（例：最適証明系の非存在）の解決が必要であることを認めている。