論文「SUPPORT IS SEARCH」の技術的サマリー

Alexander V. Gheorghiu によるこの論文は、直観主義命題論理（IPL）に対する**サンドクヴィスト（Sandqvist）の基底拡張意味論（Base-Extension Semantics: B-eS）**において、「特定の基底（base）における支持（support）」が何を意味するかという「局所的な問い」に答えることを目的としています。

著者は、支持関係が第二階のヘリディタリー・ハロップ（Hereditary Harrop）論理プログラムにおける**証明探索（proof-search）**と完全に一致することを示し、意味論の反実在論的基盤を計算論的に再解釈することに成功しました。

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

---

1. 問題設定：局所的な問いと反実在論的基盤の課題

背景:
サンドクヴィストの基底拡張意味論は、論理定項の意味をモデル論的な真理条件ではなく、推論的・証明論的な振る舞いに基づいて定義します。ここで「支持（$\Vdash_B \phi$）」は、原子文を支配する規則の集合である「基底 $B$」に対して定義されます。

• 従来の成果（グローバル）: サンドクヴィストは、「すべての基底 $B$ において $\Vdash_B \phi$ が成り立つ」ことと「$\phi$ が直観主義的に妥当である」こととの完全性を証明しました（$\Vdash_B \phi$ for all $B \iff \vdash \phi$）。
• 未解決の課題（ローカル）: しかし、「特定の基底 $B$ が固定されたとき、$\Vdash_B \phi$ は具体的に何を意味するのか？」という局所的な問いは、明確に回答されていませんでした。

課題:
支持の定義（特に論理結合子 $\lor, \to$ など）には、基底の拡張や原子に関する全称量化が含まれています。

• 例：$\Vdash_B \phi \lor \psi$ は、「任意の基底拡張 $C \supseteq B$ と任意の原子 $p$ について、$\phi \Vdash_C p$ かつ $\psi \Vdash_C p$ ならば $\Vdash_C p$」と定義されます。
• 実在論的解釈の危険性: これらの量化を「完成された無限集合（completed totality）」に対するものとして解釈すると、証明論的意味論が掲げる**反実在論的（anti-realist）**基盤（意味は公的に顕現可能な証明能力に紐づくべきであるという立場）と矛盾する恐れがあります。つまり、検証を超越した真理条件に依存してしまうという批判（シュレーダー＝ハイスターによる指摘など）が潜在的にあります。

本研究の問い:
この「完成された無限集合」への依存を排除し、支持関係を構成的で計算可能なプロセスとして再解釈することは可能か？

---

2. 手法：論理プログラミングへの符号化と CPS 変換

著者は、支持関係を第二階のヘリディタリー・ハロップ論理プログラム（Second-order Hereditary Harrop Logic）における証明探索手続きとして再定式化しました。

2.1. 原子システムと論理プログラミング

• 高次レベルの原子システム: 従来の原子システム（1 次レベルの生成規則）を拡張し、仮説を discharge する高次レベルの規則（higher-level rules）を導入します。これらは論理プログラミングにおける「節（clauses）」として表現されます。
• 第二階量化: 無限の基底拡張を扱うために、原子変数 $X$ に対する第二階量化子 $\forall X$ を使用します。これは論理プログラミングにおける「固有変数（eigenvariable）」の扱い（freshness discipline）に対応します。

2.2. 継続渡しスタイル（CPS）への解釈

支持の定義を「継続渡しスタイル（Continuation-Passing Style: CPS）」として読み替えることが鍵となります。

• 論理結合子の意味論的節は、結果を直接返すのではなく、明示的な「継続（continuation）」へ結果を渡す形式として記述できます。
• 例：$\phi \lor \psi$ の支持は、任意の原子 $p$ に対する「$\phi$ が $p$ を支持し、かつ $\psi$ が $p$ を支持するならば $p$ が支持される」という形ですが、これは論理プログラミングのゴールとして $\forall X. ((J\phi K \supset X) \supset ((J\psi K \supset X) \supset X))$ と符号化されます。

2.3. 符号化（Encoding）

各論理式 $\phi$ を論理プログラミングのゴール $J\phi K$ に符号化する関数を定義します：

• $JpK = p$
• $J\bot K = \forall X (X)$
• $J\phi \to \psi K = J\phi K \supset J\psi K$
• $J\phi \land \psi K = \forall X ((J\phi K \supset J\psi K \supset X) \supset X)$
• $J\phi \lor \psi K = \forall X ((J\phi K \supset X) \supset (J\psi K \supset X) \supset X)$

ここで、$X$ は原子変数であり、第二階量化は論理プログラムの実行（証明探索）において、新しい原子（fresh atom）を生成する操作として扱われます。

---

3. 主要な貢献と結果

3.1. 主定理（局所的な完全性と健全性）

定理 4.6: 任意の基底 $B$ と論理式 $\phi$ について、以下の同値が成り立ちます。
$$\Vdash_B \phi \iff B \vdash_O J\phi K$$
ここで、$\vdash_O$ は論理プログラミングの操作意味論（証明探索手続き）です。

• 意味: 「基底 $B$ において $\phi$ が支持される」ことは、論理プログラム $B$ に対してゴール $J\phi K$ を実行し、均一な証明（uniform proof）を見つけることと完全に一致します。
• 局所的対応: これはサンドクヴィストの「すべての基底での妥当性」というグローバルな結果を補完し、特定の基底における支持の具体的な計算的内容を明らかにします。

3.2. 反実在論的基盤の擁護

• 意味論的節に含まれる全称量化（基底拡張や原子に対して）は、完成された無限集合への参照ではなく、証明探索プロセスにおける固有変数（eigenvariable）の管理として解釈されます。
• これにより、意味論は「検証を超越した真理」に依存せず、構成的な証明探索手続きそのものとして再定義されました。これにより、証明論的意味論の反実在論的基盤が、その枠組み内でのみ一貫性を持って擁護されました。

3.3. 計算的内容の明示

• 支持関係は単に「原理的には検証可能」であるだけでなく、論理プログラミングの実行として**実際に探索可能（searchable）**であることが示されました。
• 高次レベルの原子規則（Horn 節ではない、仮説を含む節）の存在が、この対応（特に CPS 的な符号化）に不可欠であることが示されました。1 次レベルの規則に制限すると、古典論理に対応するのみで直観主義論理の構造を捉えられなくなります。

---

4. 意義と今後の展望

4.1. 理論的意義

• 意味論と計算の統合: 証明論的意味論が単なる哲学的な枠組みではなく、論理プログラミングという計算モデルと深く結びついていることを示しました。
• 実在論的仮定の排除: 意味論における「無限の集合」への依存を、動的な証明探索プロセス（固有変数の生成）に置き換えることで、反実在論的立場の純粋性を回復させました。

4.2. 実用的意義

• 実装の可能性: 支持関係が証明探索に帰着されるため、この意味論を実際のモデル化タスクや論理推論エンジンとして実装する道が開かれました。
• 古典論理への拡張: 著者は、古典論理の反実在論的基盤（二値原理なしでの正当化）において、同様の「計算的に透明な支持の定義」がまだ欠けていると指摘しています。本研究は、古典論理における同様のアプローチ（高次規則の適切な定義など）への道筋を示唆しています。

4.3. 将来的な研究方向

• 他の論理体系（線形論理、モダリティ論理など）における基底拡張意味論に対して、同様の「論理プログラミングへの符号化」と「証明探索への還元」が適用可能かという体系的な研究が期待されます。
• 適切なプログラムクラス、符号化、および均一証明の概念を特定し、証明論的意味論を統一的な計算基盤の上に再構築する作業が次のステップとなります。

---

結論

この論文は、「支持（Support）は探索（Search）である」というキャッチーな命題を、厳密な数学的証明と計算論的解釈によって裏付けました。サンドクヴィストの基底拡張意味論を、単なる意味論的な記述から、第二階論理プログラムにおける実行可能な証明探索手続きへと変換することで、証明論的意味論の反実在論的基盤を計算論的に再確立し、その実用性を大幅に高めました。