論文「Interpolation in Proof Theory」の技術的概要

この論文は、証明論的アプローチを用いた論理体系における**補間性（Interpolation）**の確立方法を包括的に概説したものです。著者らは、古典論理、直観主義論理、モダリティ論理、および構造的論理（substructural logics）など、多様な論理体系に対して、証明システム（特にシークエント計算）の構造から補間性を導出する手法を体系的に整理しています。

以下に、問題設定、手法、主要な貢献、結果、および意義について詳細をまとめます。

---

1. 問題設定 (Problem)

論理学における**補間性（Interpolation Property）**は、ある論理式 $\phi \to \psi$ が証明可能であるとき、$\phi$ と $\psi$ の共通部分の言語（変数）のみからなる論理式 $\theta$（補間式）が存在し、$\phi \to \theta$ および $\theta \to \psi$ が証明可能であるという性質です。

• クレイグ補間性 (CIP): 変数の集合が共通部分に含まれる。
• リンデン補間性 (LIP): 変数の極性（正負）も考慮される。
• 一様補間性 (UIP): 補間式が特定の文脈に依存せず、普遍的に機能する性質（二階直観主義論理における命題量化の解釈に関連）。

従来のモデル論的アプローチに加え、証明論的アプローチ（証明構造そのものから補間式を構成する）は重要ですが、以下の課題がありました：

1. 既存の手法（Maehara 法など）は、特定の証明システム（シークエント計算）に依存しており、カット除去可能なシステムがない論理には適用が困難。
2. 複雑な論理（非正規モダリティ論理や中間論理など）において、CIP や UIP が成立するかどうかの一般的な判定基準が不明確。
3. 近年発展した「普遍証明論（Universal Proof Theory）」の枠組みと、具体的な補間構成手法の統合が十分に行われていなかった。

2. 手法 (Methodology)

論文は、主に以下の 3 つの証明論的アプローチを比較・統合し、拡張しています。

A. Maehara 法（シークエント計算に基づく CIP/LIP の証明）

• 基本思想: 証明木を帰納的に走査し、各節点（シークエント）に補間式を割り当てる。
• 分割シークエント (Split Sequent): 従来のシークエント $\Gamma \Rightarrow \Delta$ を、$\Gamma; \Gamma' \Rightarrow \Delta; \Delta'$ のように「左側（$\phi$ 由来）」と「右側（$\psi$ 由来）」に分割した形式を使用。これにより、変数の条件を満たす補間式の構成を可能にする。
• 制限付きカット: 完全なカット除去が不可能な論理（例：S5）に対して、解析的カット（analytic cut）や半解析的カット（semi-analytic cut）を導入し、Maehara 法を適用可能にする。

B. Pitts 法（直観主義論理における UIP の証明）

• 基本思想: 証明探索（proof search）の過程で、特定の命題変数 $p$ を含まない「一様補間式」を再帰的に構成する。
• 特徴: 証明が終了する（強終了する）計算機システム（strongly terminating calculus）を必要とする。証明の存在ではなく、証明探索の構造そのものから補間式を抽出する。
• 拡張: モダリティ論理や中間論理へ適用され、Coq/Rocq による自動計算ツールとして実装されている。

C. 一般化されたシークエント計算への拡張

• 対象: ラベル付きシークエント（Labelled Sequent）、ハイパーシークエント（Hypersequent）、ネストシークエント（Nested Sequent）。
• 動機: 従来のシークエント計算では表現が困難な論理（例：S5 や非正規モダリティ論理）に対して、意味論的要素（Kripke モデルの到達可能性関係）を構文に直接埋め込むことで、カット除去可能かつ補間性が証明可能なシステムを構築する。
• 多項式（Multiformula）: ラベル付きシークエントでは、補間式を単なる論理式ではなく、ラベルを含んだ「多項式（multiformula）」として定義し、意味論的整合性を保つ。

D. 普遍証明論（Universal Proof Theory）との統合

• 半解析的規則 (Semi-analytic Rules): 規則の前提と結論における変数の条件を厳密に定義した規則のクラス。
• 定理: 論理が「半解析的計算機」を許容すれば CIP が、さらに「完全終了（fully terminating）」であれば UIP が保証される。逆に、補間性を持たない論理は、そのような「良い」計算機を持たないことを示す否定結果（Non-existence results）を導く。

3. 主要な貢献 (Key Contributions)

1. 包括的な手法の整理とマニュアル化:
   Maehara 法と Pitts 法の基本原理から、ラベル付きシークエントやハイパーシークエントへの拡張までを体系的に記述。読者が新しい論理に対して補間性を証明するための「逆エンジニアリング戦略（規則の形状から補間変換を導出する手順）」を提供している。

2. ラベル付きシークエントによる LIP の確立:
   従来のシークエント計算では困難だった極性（polarity）の保存（LIP）を、ラベル付きシークエントを用いて多くのモダリティ論理（S5 など）で証明可能にした。特に、S5 における LIP の証明は、従来の解析的カット法では不可能であったが、ラベル付き手法により達成された。

3. 普遍証明論による存在・非存在の決定:
   中間論理や線形論理、サブストラクチュラル論理の広範なクラスに対して、「半解析的計算機が存在するか否か」という構造的な条件と、「補間性（CIP/UIP）の成立」を結びつけた。

   • 肯定的結果: 特定の計算機構造を持つ論理は自動的に補間性を持つ。
   • 否定的結果: 補間性を持たない論理（多くの中間論理の拡張や、特定の線形論理など）は、半解析的な計算機を持たないことを示し、証明システムの限界を明らかにした。

4. 一様補間（UIP/ULIP）の新たな証明:
   Pitts 法の拡張により、モダリティ論理 K, D, T や、非正規モダリティ論理、条件付き論理などに対する一様補間性の証明論的証明を提供。また、一様リンデン補間性（ULIP）の概念を導入し、それを証明する手法を示した。

4. 結果 (Results)

• CIP/LIP の広範な適用: 古典論理、直観主義論理、モダリティ論理（K, T, D, S4, S5, GL など）、中間論理（IPC, LC, KC など）、サブストラクチュラル論理（FL, MALL, ILL など）の多くで CIP/LIP が成立することが再確認・証明された。
• 非存在定理: 補間性を持たない論理（例：多くの中間論理の拡張、特定の線形論理の拡張、非正規モダリティ論理の EC, ECN など）は、半解析的な計算機を持たないことが示された。これは、これらの論理に対して「良い」証明システム（カット除去可能で構造的に単純なシステム）が存在しないことを意味する。
• S5 と LIP: 従来のシークエント計算では LIP の証明が難しかった S5 に対して、ラベル付きシークエント計算を用いることで LIP が成立することを示した。
• 自動化: Pitts 法のアルゴリズムが Coq/Rocq で実装され、一様補間式の自動計算が可能になったことが報告されている。

5. 意義 (Significance)

• 証明論と意味論の架け橋: 補間性という論理的性質を、証明システムの構造的な特徴（規則の形状、終了性、カットの制限）と直接結びつけることで、論理の「良質さ（well-behavedness）」を証明論的に特徴づける枠組みを提供した。
• 計算可能性と複雑性: 補間式の構成が証明のサイズに対して線形であるなど、計算複雑性の観点からも有用である。また、NP と coNP の関係など、計算量理論への応用可能性も示唆されている。
• 新しい証明システムの設計指針: 「補間性を持たない論理は、半解析的な計算機を持たない」という否定結果は、新しい論理を設計する際、あるいは既存の論理の証明システムを構築する際の重要な指針となる。
• 実用的なツール: 補間式の構成アルゴリズムが明確に提示されており、定理証明支援系や論理推論ツールへの実装への道筋が開かれた。

総じて、この論文は、証明論的アプローチが単なる存在証明にとどまらず、具体的な構成アルゴリズムを提供し、かつ論理体系の構造的特性を深く理解するための強力な枠組みであることを示す重要な貢献です。