Four intuitionistic modal connectives

技术摘要：四种直觉主义模态联结词

问题陈述
本文探讨了直觉主义模态逻辑（IMLs）的基础语义学与公理化。传统上，IMLs 在关系结构 $(W, \leq, R, V)$ 中解释模态联结词，其中 $\leq$ 是一个预序，而 $R$ 是一个二元关系。在关于可能性算子的两种主要思想流派之间存在着核心张力：

1. Fischer Servi 的方法： 定义可能性 ($\diamond_{FS}$) 为：$s \models \diamond_{FS} A$ 当且仅当存在 $t$ 使得 $sRt$且$t \models A$。这种方法通常需要将模型类限制为“前向与后向汇合”（forward and backward confluent）的框架，以满足遗传性质（对 $\leq$ 的单调性）。
2. Wijesekera 的方法： 定义可能性 ($\diamond_{W}$) 为：$s \models \diamond_{W} A$ 当且仅当对于所有 $t \geq s$，都存在 $u$ 使得 $tRu$且$u \models A$。这种方法并不严格要求汇合性来保证遗传性质成立。

作者认为，将讨论限制在汇合模型（如 Fischer Servi 所做的那样）是一种武断的选择，这优待了直觉主义一阶逻辑的某种特定变体。此外，他们指出，如果仅限于汇合模型，将 IMLs 标准翻译为一阶逻辑的方法往往无法捕捉到预期的语义。因此，本文旨在建立一个统一的框架，该框架包含四种不同的模态联结词，而不预先限制框架的类别，从而探索直觉主义模态性的完整图景。

方法论
作者采用了一种结合关系语义学、对应理论、代数证明系统和模型论技术的严谨方法：

1. 语法与语义：

   • 他们引入了一种包含标准直觉主义联结词 ($\to, \top, \bot, \lor, \land$) 以及对偶蕴涵/共蕴涵 ($\leftarrow$) 的语言。
   • 定义了四种模态算子：
     • $\Diamond$ (Přenosil 式的可能性)：$s \models \Diamond A$ 当且仅当 $\exists t \leq s, \exists u (tRu \land u \models A)$。
     • $\Box$ (Fischer Servi 式的必然性)：$s \models \Box A$ 当且仅当 $\forall t \geq s, \forall u (tRu \to u \models A)$。
     • $\Diamond$ (Wijesekera 式的可能性)：$s \models \Diamond A$ 当且仅当 $\forall t \geq s, \exists u (tRu \land u \models A)$。
     • $\blacksquare$ (对偶必然性)：$s \models \blacksquare A$ 当且仅当 $\exists t \leq s, \forall u (tRu \to u \models A)$。
   • 语义是在所有框架类上定义的（不设汇合限制），并且证明了所有公式在这些定义下均满足遗传性质。

2. 对应理论：

   • 本文研究了基本框架类的模态可定义性（例如：序列、自反、对称、传递、汇合）。
   • 利用符号公式（signed formulas）和推理规则来刻画框架属性。
   • 利用模型论中的“相对化性质”（Relativization Property）来证明某些框架类的模态可定义问题是不可判定的。

3. 公理化与完备性：

   • 提出了一个使用符号公式集合（正向与负向）的希尔伯特风格系统，该系统对统一替换以及特定的推理规则（包括对偶蕴涵和模态间相互作用的规则）封闭。
   • 作者使用“平衡夹点”（balanced clips，由素滤子、素理想及辅助公式组成的三元组）构建了规范模型（Canonical Model）。这种构造对于处理四种模态与对偶蕴涵之间复杂的相互作用是必要的。
   • 为最小逻辑及其对应于特定框架类（自反、序列、前向/向下汇合）的扩展逻辑证明了完备性定理。

4. 可判定性：

   • 为了证明可判定性，作者将最小 IML 嵌入到经典一阶逻辑的单元二变量卫语句片段（Monadic Two-Variable Guarded Fragment）中。
   • 他们定义了将直觉主义公式映射到卫语句一阶公式的翻译函数，利用了卫语句片段已知的可判定性。

关键贡献与结果

• 统一框架： 本文成功地将四种不同的模态联结词 ($\Diamond, \Box, \Diamond, \blacksquare$) 集成到一个单一的直觉主义框架中，并证明了它们在所有框架类上不是互定义的。
• 消去分析： 研究表明，在正向且向下汇合的框架类 ($C_{fd}$) 上，所有四种联结词都是可消去的（即互定义的）。然而，在更广泛的类别（如 $C_{bdu}$）上，它们是不同的。
• 对应结果：
  • 前向汇合 ($C_f$) 和向下汇合 ($C_d$) 框架类是正向可定义的。
  • 自反 ($C_{ref}$)、对称 ($C_{sym}$)、传递 ($C_{tra}$)、欧几里得 ($C_{Euc}$) 和确定性 ($C_{det}$) 框架类相对于所有框架类（或特定子类如 $C_{fbdu}$）是不可模态可定义的。
  • 后向汇合 ($C_b$) 和向上汇合 ($C_u$) 框架类相对于 $C_{fd}$ 是不可模态可定义的。
• 公理化： 本文为最小逻辑 ($L_{min}$) 及其对应于自反性、序列性和汇合性的扩展逻辑提供了完备公理化。最小逻辑被证明是所有框架的逻辑。
• 可判定性： 最小直觉主义模态逻辑 ($L_{min}$) 及其若干扩展（自反、序列、汇合）的成员问题被证明是可判定的。这是通过将问题归约为单元二变量卫语句一阶逻辑的可满足性问题来实现的。
• 可定义性的不可判定性： 本文证明了确定一个基本类框架是否为模态的、正向的或负向可定义的判定问题是不可判定的。

意义与主张

作者声称，通过避免将讨论武断地限制在汇合模型上，他们的工作为 IMLs 提供了一个更自然且约束更少的基石。通过引入对偶蕴涵和四种模态联结词，他们提供了一个对称且全面的语言，能够捕捉到全范围的直觉主义模态行为。

文中谦虚地指出，虽然建立了最小逻辑的可判定性，但该问题的复杂度类仍是一个开放问题。此外，作者强调，虽然在完备性证明中使用了某些推理规则（特别是 $R8+$ 和 $R8-$），但目前尚不清楚这些规则是否可以被有限的公理集所取代。他们还针对对称和传递框架对应的逻辑是否具有有限公理化问题，以及将过滤技术应用于此特定环境的可能性提出了开放性问题。

这项工作为理解不同直觉主义模态语义及其相应框架属性之间的相互作用奠定了基础性的步骤，超越了传统的 Fischer Servi 与 Wijesekera 的二分法。