Towards Automated Proof-Theoretic Semantics: Inference-Behaviour Semantics for 3-Dimensional K3 and LP

技術要約：自動化された証明論的意味論に向けて：3次元K3およびLPに対する推論挙動意味論

問題提起
論理的推論の自動化（例：分解法、定理証明器、およびRocqやLeanのような対話型アシスタントによるもの）は確立されているが、そのような推論のための「証明論的意味論（P-tS）」を自動的に提供することは、依然として未解決の課題である。MUltlogのようなシステムは、モデル論的な真理値表から任意の有限値論理に対するシーケント計算、タブロー、および自然演繹システムを自動生成できるが、それらのシステム内の結合子の意味仕様を生成するという逆の能力を欠いている。既存のP-tSのアプローチ（証明論的妥当性や基底拡張意味論など）は、多くの場合、計算（calculus）に依存しており、異なる論理間（例：古典論理と直観主義論理）で結合子の意味を比較することを妨げている。本論文は、結合子の意味をその最小限の推論挙動によってモデル化する「推論挙動意味論（I-bS）」のアプローチをMUltlogフレームワークに統合し、多値論理に対するP-tSの生成を自動化することを目指している。

方法論
本論文は、以前は2次元のシーケント計算に限定されていたI-bSフレームワークを、$n$次元のシーケント計算へと拡張する。手法は以下のステップで進行する：

1. 形式的装置： 著者は、$n$次元シーケントを論理式のマルチセットの$n$組として定義する。これらをモデル論的な真理値に依拠せずに解釈するために、著者らは「多角的（multilateralist）」な読み方を採用する。3次元シーケント（具体的には強クリーネ論理（K3）およびパラドックスの論理（LP））の場合、これには3つの発話行為（主張（第1次元）、判断の中断（第2次元）、および否定（第3次元））が含まれる。
2. 最小派生関係： 特定の論理の構造的特徴から結合子の意味を分離するため、著者は恒等式（$Id_3$）と制限されたカット規則（$Cut_2$）からなる最小派生関係を定義する。これにより、標準的な計算に見られる完全な構造規則（縮約や弱化など）による「混同」の影響を回避する。
3. 定義可能性と推論挙動： ベルナップ流の定義に従い、結合子は、それが基底となる計算を保守的に拡張し、かつ対応するものと一意に相互派生可能である場合に定義される。核心となる指標は、定義の証明中における結合子の水平方向の位置（次元）と規則の適用を追跡する関数である「推論挙動（$ib$）」である。
4. 意味の拡張： 異なる次元性を持つ結合子間（例：2次元の古典論理と3次元のパラコンシステント論理）で比較するために、本論文では「意味の拡張」を導入する。ある$m$次元の結合子が$n$次元の結合子の意味を拡張するとは、$m > n$ の場合において、前者の$n$次元の断片内において後者の推論挙動が保守的に保持されることを指す。

主要な貢献と結果
本論文は、MUltlogによって生成された3次元シーケント計算を用いて、2つの3値論理（K3およびLP）にこの拡張されたフレームワークを適用する。

• K3/LPの意味節（Semantic Clauses）： 著者は、最小限の $\{Id_3, Cut_2\}$ 関係に対して、乗法的および加法的バージョンのK3結合子のユニークネス（一意性）と保守性を証明する。著者らは、各結合子のバージョン（例：乗法的連言 $\otimes$ 対 加法的連言 $\sqcap$）に対して異なる意味節を導出し、標準的なK3計算がその構造規則によって意味的に異なる結合子を混同していることを示している。
• K3とLPの意味の一致： 中心的な結果は、K3とLPの結合子が同一の意味を持つことである。K3とLPは指定値（K3は第3次元のみを指定し、LPは第2および第3次元を指定する）において異なるが、それらの垂直的な派生特性および操作規則は同一である。したがって、定義の証明におけるそれらの推論挙動は同一であり、同じ意味節をもたらす。
• 古典論理の意味拡張： 本論文は、K3およびLPの3次元結合子が、LK（2次元）における古典的な結合子の意味拡張であることを示している。3次元の意味節を第1および第3次元に投影（第2次元を除去）することにより、得られる規則は古典的なLKの結合子の意味節と構文的に同一になる。これは、K3/LPの結合子が、その意味を変えることなく古典的な意味を保守的に拡張していることを裏付けている。
• 構造規則の取り扱い： 分析により、最小限の推論挙動を維持するためには、文脈の制限（例：シーケントの構成要素における論理式の数の制限）が必要であることが明らかになった。これらの制限がない場合、標準的な構造規則（縮成立など）は推論挙動を変化させ、事実上、結合子の意味を変えてしまう。

意義と主張
本論文は、I-bSを2次元より大きい次元へと拡張するための最初の基礎的なケーススタディを提供すると主張している。その主要な意義は以下の通りである：

1. クロス・カルキュラス比較： 異なる次元性を持つ論理間の結合子の意味を比較するメカニズムを確立した。これは、異なる構造的特性を持つ論理の比較に苦慮してきた従来のP-tS文献におけるギャップに対処するものである。
2. 論理多元論の検証： K3とLPが同一の結合子の意味を共有しているという発見は、異なる指定値や妥当性条件を持つにもかかわらず、異なる論理が同じ結合子の意味を共有し得るという、証明論的な論理多元論の視点を支持するものである。
3. 自動化への道： 3次元計算をI-bSにマッピングすることに成功したことで、本論文はI-bSをMUltlogに統合するための基礎を築いた。最終的な目標は、任意の有限値論理に対する証明論的意味論の生成を自動化することである。著者は、現在の作業は手動によるケーススタディであることを認めつつも、フレームワークは計算的に実装できるように設計されており、任意の多値論理に対する証明論的意味論の自動生成を可能にする可能性があるとしている。

著者は、任意の$n$次元計算に対する必要な定義の証明を生成することが計算上の課題として残っていることを認めつつも、自動化の全プロセスに関する即時的な自動化については控えめな姿勢を保っている。