Modal Extensions of CLoN with Bi-neighborhood Semantics

技術要約：Bi-neighborhood Semanticsを用いたCLoNの様相拡張

問題提起
本論文は、FDE（First Degree Entailment）のサブシステムであるCLoN（否定に関してギャップ（欠落）とグルット（過剰）の両方を持つ古典論理）に基づく、非正規様相論理を構築するという課題に取り組んでいる。CLoNは、否定演算子（$\neg$）を備えた正の古典論理として特徴付けられるが、この否定は特定の公理や意味論的な偽（falsity）の条件を持たない。その結果、CLoNにおける$\neg$は合同的（congruential）ではなく（置換特性を満たさない）、この論理はパラコンシステント（矛盾許容的）かつパラコンプリート（不完全許容的）である。

CLoNベースのシステムの様相拡張に関する既存のアプローチは、最初から強い公理（公理Kなど）を仮定するか、あるいはクリプキ意味論を利用することが多いが、これらは特定の哲学的な応用（義務論理など）にとっては制約が強すぎる場合がある。さらに、否定の偽の条件が欠如しているため、CLoNにおいては必然性（$\Box$）と可能性（$\Diamond$）の間の標準的な双対性を定義することができない。著者らは、弱形式の否定を、システムを自明化させることなく受け入れつつ、特に相反する義務を扱う必要がある道徳的ジレンマのようなアプリケーションにおいて、体系的かつ最小限の近傍意味論をCLoNに提供することに関する文献上の空白を特定している。

方法論
著者らは、FDEベースの非正規様相論理（Dalmonte et al., 2018; Drobyshevich and Skurt, 2021）に関する先行研究から適応されたフレームワークである、bi-neighborhood semantics（二重近傍意味論）を採用している。この手法は、以下の主要な構成要素を含む。

1. 基底論理 (CLoN, CLuN, CLaN): 命題の基底は、正の古典公理を含むが否定に関する規則を持たないヒルベルト計算式によって定義される。意味論的には、著者らは検証（verification）と拒絶（rejection）の条件を表すペア $(v_1, v_2)$ を用いたswap structures（非決定論的行列）を利用する。

   • CLoN: 検証と拒絶の関係に制約を持たない基底システム。
   • CLuN: 排中律（$\phi \lor \neg \phi$）を加えることで得られ、すべての世界が公式を検証または拒絶することを強制する（パラコンシステント）。
   • CLaN: 爆発原理（$\phi \to (\neg \phi \to \psi)$）を加えることで得られ、どの世界も公式を同時に検証および拒絶しないことを強制する（パラコンプリート）。

2. Bi-neighborhood Frames: 様相論理 CLoNE は、フレーム $\mathcal{W} = \langle W, N^+_2, N^+_3 \rangle$ （および後に $N^-_2, N^-_3$ を用いて拡張）を用いて定義される。

   • 検証集合 ($[\phi]^+$): 近傍関数 $N^+$ を通じて定義される。ここで、$w \in [\Box \phi]^+$ であるとは $[\phi]^+ \in N^+_2(w)$ であることと同義である。
   • 拒絶集合 ($[\phi]^-$): 別の独立した近傍関数 $N^-$ を通じて独立に定義される。決定的なのは、弱形式の否定のために、様相公式の拒絶集合は検証集合から導出されない点である。代わりに、$[\Box \phi]^-$ は $\{w \in W \mid [\phi]^- \in N^-_2(w)\}$ として定義される。
   • 独立性: $\Box$ と $\Diamond$ は、双対としてではなく独立に定義される。これにより、標準的な双対公理を必要とせずに、否定された様相（例：$\neg \Box \phi$）を扱うことが可能となる。

3. 外延性規則: システムは正の部分集合に対して外延性規則（$\phi \leftrightarrow \psi / \Box \phi \leftrightarrow \Box \psi$）を採用するが、弱形式の否定が否定された公式の合同性を妨げることを認めている。否定された様相を扱うために、システムは否定に関する特定の外延性規則 $\neg \phi \leftrightarrow \neg \psi / \neg \Box \phi \leftrightarrow \neg \Box \psi$ を導入する。

4. 証明体系: 著者らは、bi-neighborhood フレームのクラスに対する CLoNE およびその拡張の健全性と完全性を確立している。完全性の証明には、素な理（prime theories）から構成された標準モデルが用いられる。

主な貢献と結果

• CLoNE の定式化: 本論文は、健全かつ完全な bi-neighborhood 意味論を備えた、CLoN の最小限の非正規様相拡張である CLoNE を提示している。
• 弱形式の否定の処理: 拒絶集合を様相演算子に対して独立に定義することで、弱形式の否定演算子を含む非自明な公理を検証することに成功した。これにより、古典的な双対性に崩壊することなく、否定された様相を表現できる。
• 公理的拡張: 著者らは、様々な公理的拡張（M, C, K, T, 4, D 等）をフレームの性質として特徴付けている。
  • 正の拡張: M（増強）や C（閉包）といった標準的な公理は、検証近傍関数の性質に対応する。
  • 否定された拡張: 否定を含む新しい公理（例：$M^-, C^-, T^-$）は、検証と拒絶の近傍関数間の特定の相互作用に対応することが示されている。
• マルチモーダル能力: 本フレームワークは、異なる様相（例：義務と可能性）が、架け橋となる原理（相互作用公理）によってのみ接続され、独立した近傍関数によって制御されるマルチモーダル・システムをサポートしている。
• 完全性: 論文では、CLoNE およびその標準的な拡張が、それぞれのフレームのクラスに対して健全かつ完全であることを証明している。

意義と主張
著者らは、本研究が、道徳的ジレンマを自明化させることなく受け入れることができる義務論理のための必要な意味論的基礎を提供すると主張している。

• 道徳的ジレンマ: 標準的な義務論理において、真の道徳的ジレンマ（解決不可能な相反する義務）の存在は、集約（公理C）や爆発原理といった標準的な原理と組み合わさった際、しばしば論理的爆発（自明化）を招く。
• パラコンシステンシー: CLuN（CLoN の拡張）に基づいていることにより、本フレームワークは、任意の結論を導出することなく、相反する義務（$O\phi$ と $O\neg\phi$）の共存を許容する。
• 様相の独立性: Bi-neighborhood アプローチにより、古典的な双対性に依存しない、異なる様相的概念（例：義務 vs 形而上学的可能性）をモデル化できる。これは、義務が撤回不可能であり、標準的な論理的解決が失敗するシナリオを定式化する上で極めて重要である。
• 哲学的有用性: 本論文は、弱形式の否定が特定の古典的な推論を制限する一方で、まさにこの特徴こそが、他のパラコンシステント義務論理（LFI など）に見られるような「人工的な」整合性演算子の導入を回避しつつ、解決不能な道徳的状況を自然にモデル化することを可能にすると論じている。

結論として、提案されたフレームワークは、様相公理へのコミットメントを最小限に抑えつつ、矛盾を含む道徳的推論に関する非標準的な哲学的立場を探索するための、柔軟で数学的に厳密なツールを提供するものである。