A Proof-theoretic Semantics for Intuitionistic Linear Logic

問題設定
証明論的意味論（P-tS）は、真理ではなく証明の概念を通じて論理式の意味を付与することを目指している。Sandqvistが直観主義命題論理（IPL）に対して基底拡張意味論（B-eS）を確立し、Gheorghiu, Gu, および Pym がこれを直観主義線形論理の乗法的断片（IMLL）へと拡張したが、完全な直観主義線形論理（ILL）に対する P-tS の構築は依然として困難な課題であった。主な課題は、弱化や縮約を一般に禁止する ILL の部分構造的な性質と、加法的結合子および指数型モダリティ（！）の包含にある。既存のアプローチは、ベース拡張の枠組みの中でこれらの特徴の相互作用を扱うことに苦慮している。具体的には、資源に敏感な ILL の性質を尊重しつつ、「バング（!）」と呼ばれるモダリティ（厳密な導出を要求する指数型演算子）の推論的内容を正しく捉えるためのサポート関係を定義することは、大きな困難を伴う。さらに、標準的な ILL の自然演繹システムは、しばしば文脈共有（加法性）や前提の数の変動に関するアドホックな側条件に依存しており、これらは B-eS で要求される非図式的で厳格な原子規則の構造内では形式化が困難である。

手法
本論文は、自然演繹規則の図式的な文脈メタ変数を用いない形式化と、加法性とモダリティを扱うサポート関係の定義という、2つの主要な技術的ハードルに対処することで、ILL に対する新しいベース拡張意味論を提案する。

1. 自然演繹の再定式化： 著者は、「加法的ボックス」（{...} で表記）と「モダル・ボックス」（J...K と表記）を用いた自然演繹システム NILL の新しい構文を導入する。

   • 加法的ボックス： これらは共有文脈を画定し、文脈のメタ変数に依存することなく、加法的結合子（& や ⊕ など）や可変個数の前提を持つ規則（⊤I や 0E など）を表現することを可能にする。これにより、ボックス内の導出が同じ開いた仮定のマルチセットを共有するという、加法性の体系的な扱いが可能になる。
   • モダル・ボックス： これらは昇格規則（Prom）を特徴付けるために使用される。この規則は、結論が、その上にあるすべてのモダル・ボックスを含む規則から導かれる仮定からなる文脈から導かれることを要求するように再定義される。これにより、規則の構造的定義の中で ! 結合子に明示的に言及することなく、指数型モダリティの厳密な導出要件を捉えることができる。
   • 著者は、この新しいシステムが標準的なシーケント形式の NILL と等価であることを証明している（定理 2.7）。

2. 原子的導出可能性とサポート関係：

   • 原子規則： 意味論における原子規則は、加法的ボックスのマルチセット、単一の加法的ボックス（結論）、および原子からなるトリプルとして定義される。これは、再定式化された自然演繹規則の構造を反映している。
   • 基底拡張： 基底 $B$ は、このような原子規則の集合である。導出関係 $\vdash_B$ は、文脈の乗法的分割と、ボックス構造による加法的共有を扱うように帰納的に定義される。
   • サポート関係 ($\Vdash_B^L$)： 支持関係の核となる定義は、ILL へと拡張される。決定的なことに、指数型モダリティ !ϕ の節は、単なる構造的規則としてではなく、基底拡張にわたる $\phi$ の妥当性に関する条件として定義される。具体的には、任意の拡張 $C$ が $B$ のとき、もし $\phi$ が $C$ の「定理」である（すなわち、すべての $D \supseteq C$ に対して $\Vdash_D^\emptyset \phi$ である）ならば、そのリソースを使用できる、という形で $\Vdash_B^L !\phi$ が成立する。
   • モダリティの扱い： 本論文では、基底における「永続的原子（persistent atoms）」の概念を導入する。これらは !ϕ の形の論理式に対応する。これらの原子は、標準的な仮定と、弱化や縮約が可能な仮定を区別する役割を果たし、支持関係における ! 結合子の役割を担う。

主要な貢献

• ILL に対する完全な B-eS： 本論文は、加法的結合子および指数型モダリティを含む、完全な直観主義線形論理をカバーする最初のベース拡張意味論を提示する。
• 加法性の体系的な扱い： 加法的ボックスを導入することにより、著者は、アドホックな側条件や明示的な文脈メタ変数を用いることなく、文脈共有や可変前提規則を扱う手法を提供している。これは、推論図形のよりクリーンで一様な表現を提供する。
• モダル・ボックスによる特徴付け： モダル・ボックスを用いた昇格規則の再定義は、特定の結合子の構文に依存しない指数型モダリティの構造的特徴付けを提供し、ベース拡張の枠組みへの統合を容易にする。
• ! の推論主義的説明： 本論文は、! 結合子の推論主義的内容について詳細な議論を行っている。意味論は、! を基底拡張における論理式の妥当性に関する条件として扱うことで、モダリティの「必然化」の側面を内部化し、! のモダルな性質を捉えていると主張している。
• 健全性と完全性： 提案された意味論が自然演繹システム NILL に対して健全かつ完全であることを証明する。完全性の証明には、原子規則が NILL の推論規則を模倣する「シミュレーション基底」 $N$ を構築し、フラットニング写像を用いて ILL 論理式を原子へと変換するプロセスが含まれる。

結果

• 定理 2.7： 標準的なシーケント形式の導出可能性 ($\vdash$) と、新しいボックスベースの導出可能性 ($\vdash^*$) との間の等価性を確立する。
• 定理 5.1（健全性）： もしシーケントが NILL で証明可能ならば、提案された意味論において妥当である ($\Gamma \vdash \phi \implies \Gamma \Vdash \phi$) ことを証明する。
• 定理 6.1（完全性）： もしシーケントが意味論において妥当ならば、NILL で証明可能である ($\Gamma \Vdash \phi \implies \Gamma \vdash \phi$) ことを証明する。
• 定理 4.15： ! を持つ仮定を扱うために使用される特定の (Inf) 節が、より一般的な (Gen-Inf) 節と等価であることを示し、モダルな仮定の特定の扱いを正当化する。
• 系 4.11 および 4.12： ! とサポート関係の相互作用に関する構造的性質を確立し、$\phi$ が妥当であれば !ϕ も妥当であること、および !Γ が !ϕ をサポートするならば ϕ をサポートすることも示す。

意義
本論文は、B-eS のアプローチを IPL および IMLL から完全な ILL へと拡張することにより、証明論的意味論における重要な空白を埋めるものであると主張している。著者は、Gheorghiu, Gu, および Pym が乗法的断片の処理に成功した一方で、加法的要素と指数型モダリティの追加には大幅な新しい仕組みが必要であったと述べている。本研究は、モダリティに対する固有の証明論的アプローチにおいて重要であり、! という結合体を単なる構造的規則としてではなく、ベース拡張の枠組み内における論理式の妥当性に関する条件として理解するための道を開くものである。著者は、昇格規則と加法性を扱うための解決策が「いくぶん複雑（convoluted）」であることを認めつつも、推論図形のクリーンで体系的な表現を実現するためには必要であったとしている。さらに、本論文は、Sandqvist の IPL 意味論をこの ILL フレームワークに直接埋め込むことの困難さを強調しており、両者の間のマッピングの一般化を将来の研究における未解決問題として残している。本研究は、P-tS における現在のモダリティへのアプローチには、ようやく対処され始めたばかりの、深い形而上学的または構造的な洞察が必要である可能性を示唆している。