Modal Extensions of CLoN with Bi-neighborhood Semantics

技术摘要：基于双邻域语义的 CLoN 模态扩展

问题陈述
本文解决了基于 CLoN（关于否定而言具有空缺与矛盾特性的经典逻辑）构建非正规模态逻辑的挑战。CLoN 是 FDE（一阶蕴涵）的一个子系统，其特征是作为正向经典逻辑，并增加了一个缺乏特定公理或语义虚假条件的否定算子 ($\neg$)。因此，CLoN 中的 $\neg$ 不是符合性的（它不满足替换性质），且该逻辑既是次协调的（paraconsistent），也是次完备的（paracomplete）。

现有的 CLoN 模态扩展方法通常从一开始就假设强公理（如公理 K），或利用 Kripke 语义，这对于某些哲学应用（如义务逻辑）来说可能过于严格。此外，由于缺乏否定的虚假条件，CLoN 中无法定义必然性 ($\Box$) 与可能性 ($\Diamond$) 之间的标准对偶关系。作者指出，文献中存在一个空白，即缺乏一种系统性的、最小化的 CLoN 邻域语义，能够容纳其弱否定而不使系统平凡化，特别是在处理必须处理冲突义务而不导致爆炸的道德困境应用方面。

研究方法
作者采用了双邻域语义（bi-neighborhood semantics），这是一个借鉴自先前关于基于 FDE 的非正规模态逻辑研究（Dalmonte 等，2018；Drobyshevich 和 Skurt，2021）而改编的框架。该方法包含以下关键组成部分：

1. 基础逻辑 (CLoN, CLuN, CLaN)： 命题基础通过包含正向经典公理但没有否定规则的希尔伯特演算来定义。在语义上，作者利用交换结构（swap structures，非确定性矩阵），其中真值是代表验证和拒绝条件的对 $(v_1, v_2)$。

   • CLoN： 基础系统，验证与拒绝之间没有任何约束。
   • CLuN： 通过添加排中律 ($\phi \lor \neg \phi$) 获得，强制要求每个世界要么验证要么拒绝一个公式（次协调）。
   • CLaN： 通过添加爆炸原理 ($\phi \to (\neg \phi \to \psi)$) 获得，强制要求没有任何世界既验证又拒绝一个公式（次完备）。

2. 双邻域框架： 模态逻辑 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. 证明系统： 作者建立了 CLoNE 及其扩展相对于双邻域框架类的可靠性和完备性。他们利用通过素理论（prime theories）构建的规范模型来证明完备性。

主要贡献与结果

• CLoNE 的形式化： 本文提出了 CLoNE，即 CLoN 的最小非正规模态扩展，并配备了可靠且完备的双邻域语义。
• 处理弱否定： 该框架通过为模态算子定义独立的拒绝集，成功验证了包含弱否定算子的非平凡公理。这使得在不坍缩为经典对偶的情况下表达否定模态成为可能。
• 公理化扩展： 作者根据框架属性刻画了各种公理化扩展（M, C, K, T, 4, D 等）。
  • 正向扩展： 标准公理如 M（增广性）和 C（封闭性）对应于验证邻域函数的属性。
  • 否定扩展： 涉及否定的新公理（如 $M^-$, $C^-$, $T^-$）被证明对应于验证邻域函数与拒绝邻域函数之间的特定相互作用。
• 多模态能力： 该框架支持多模态系统，其中不同的模态（例如义务与可能性）受独立的邻域函数支配，仅通过特定的桥接原理（如相互作用公理）相连。
• 完备性： 本文证明了 CLoNE 及其规范扩展相对于其各自框架类的可靠性和完备性。

意义与主张
作者声称，这项工作为能够容纳道德困境而不导致平凡化的义务逻辑提供了必要的语义基础。

• 道德困境： 在标准义务逻辑中，真实的道德困境（无法解决的冲突义务）的存在，在与聚合（公理 C）或爆炸原理结合时，往往会导致逻辑爆炸（平凡化）。
• 次协调性： 通过将系统建立在 CLuN（CLoN 的一个扩展）之上，该框架允许冲突义务（$O\phi$ 和 $O\neg\phi$）共存，而不会推导出任意结论。
• 模态独立性： 双邻域方法允许对不依赖于经典对偶的截然不同的模态概念（例如义务与形而上学可能性）进行建模。这对于形式化那些义务并非可撤销且标准逻辑解决手段失效的情景至关重要。
• 哲学效用： 作者认为，虽然弱否定限制了某些经典推理，但这恰恰是该系统能够自然地模拟“无法解决”的义务情境、避免引入其他次协调义务逻辑（如 LFI）中常见的“人工”一致性算子的特征。

论文结论指出，所提出的框架提供了一个灵活且数学严谨的工具，用于探索非标准哲学立场，特别是涉及道德推理中矛盾的情况，同时保持对模态公理的最小承诺。