Conditionals and Modalities in Constructive Quantum Logics

技术摘要：构造性量子逻辑中的条件与模态

问题陈述
本文旨在解决将构造性推理（直觉主义逻辑）与量子推理（正交模态逻辑）统一在单一命题框架内的挑战。由 Holliday 引入的“基本逻辑”（fundamental logic）通过扩展签名 $\{\land, \lor, \neg\}$ 对两者进行了泛化，但它缺乏稳健的蕴含概念。正交逻辑（最小量子逻辑）通常缺乏满足模даus ponens（假定前件）的条件，而直觉主义逻辑则高度依赖蕴含联结词。

作者研究了直觉主义逻辑与配备了 Sasaki 蕴含（定义为 $a \to b := \neg a \lor (a \land b)$ 的正交模态逻辑）的交集。核心问题是在全签名 $\{\land, \lor, \to\}$ 中，如何对这两个系统同时有效的公式集进行公理化。先前的研究已经确定，直觉主义逻辑与正交逻辑（不含蕴含）的交集严格大于基本逻辑，并由公理 (Ex) 进行公理化。本文寻求将这一结果扩展到包含蕴含的情况。

方法论
作者采用了代数方法，利用了 基本代数（fundamental algebras，即泛化了 Heyting 代数和正交模态格的结构）理论。其方法论分为三个主要阶段：

1. 代数定义： 作者定义了 Ex-代数，这是一类泛化了正交模态代数（配备 Sasaki 蕴含）和 Heyting 代数的基本代数。这涉及引入一个新的公理 (iEx)（“蕴含式 Ex”），它将早期的 (Ex) 公理扩展到了蕴含签名。他们还定义了辅助公理 (nS, MP, M, W4) 来捕捉 Sasaki 蕴 hàm 的行为以及 modus ponens。
2. 嵌入定理： 核心技术贡献是 iEx-嵌入定理。作者证明了任何 Ex-代数 $L$ 都可以亚直积地嵌入到正交模态代数 ($O_L$) 与 Heyting 代数 ($I_L$) 的积中。
   • 正交模态分量 $O_L$ 是通过由等价关系 $a \sim b \iff \neg a = \neg b$ 定义的 $L$ 的商空间构建的。
   • Heyting 分量 $I_L$ 是通过使用素滤子和开集拓扑进行表示来构建的，类似于 Stone 表示分配格的方法。
   • 至关重要的是，作者证明了蕴含联结词在这些同态下是保持的，特别是展示了商空间中的 Sasaki 蕴含与正交模态代数中的定义相一致。
3. 模态扩展： 该框架被扩展到了包含模态算子 ($\Box, \Diamond$) 的情况。作者定义了 miEx 代数（模态 iEx 代数）以及相应的模态代数类：IFS 代数（直觉主义 Fischer Servi 代数）和 DOM 代数（分配正交模态代数）。他们证明了一个模态版本的嵌入定理，表明 miEx 代数可以嵌入到 DOM 代数与 IFS 代数的积中。

主要贡献与结果

• 交集的公理化： 本文为直觉主义逻辑与正交模态逻辑（带 Sasaki 蕴含）的共同有效逻辑提供了完整的公理化。该逻辑被称为 iEx-逻辑，被证明是这两个系统的交集。
  • 定理 1.1 & 4.2： 该交集在基本逻辑之上由公理 (iEx) 以及另外四个原则进行公理化：
    1. $\neg(a \to b) = \neg(\neg a \lor (a \land b))$ (nS)
    2. $a \land (a \to b) = a \land b$ (MP)
    3. $(a \land b) \to b = 1$ (M)
    4. $a \to (b \land c) \le a \to b$ (W4)
  • 作者还提供了一种替代公理化方案，将 (iEx) 分解为三个公理：(Nu)、(Vi) 和 (iCl)，连同蕴含特定公理一起。
• 扩展格的特征描述： 一个主要的结构性结果是对所有扩展 iEx-逻辑的逻辑（ICQ 逻辑）的格进行的特征描述。
  • 定理 4.6： ICQ 逻辑的格同构于超直觉主义逻辑格与超正交模态逻辑格的积（$iSE \simeq iSO \times iSI$）。这意味着任何 iEx-逻辑的扩展都由其在直觉主义和正交模态分量上的投影唯一确定。
• 模态逻辑交集： 本文确立了特定类别的直觉主义模态逻辑 (IFS) 与量子模态逻辑 (DOM) 的交集恰好是 miEx 代数的逻辑（推论 5.11）。这是通过限制模态算子以满足特定的分配性和对合性质（例如，公理 I1 和 M3）来实现的，这些性质确保了商映射能够保持模态结构。

意义与主张
本文回答了一个关于当使用 Sasaki 蕴含时，直觉主义与正交模态逻辑的“共同有效原则”的具体问题。通过引入 Ex-代数和 iEx-嵌入定理，作者证明了这两个截然不同的逻辑传统之交集不仅仅是一个弱组合，而是一个可以清晰分解为其组成部分的结构化系统。

其意义在于：

1. 统一性： 为包括蕴含（这是一个此前难以与非分配性的量子逻辑相调和的特征）的“构造性量子逻辑”提供了一个严谨的代数和公理化框架。
2. 结构清晰性： 扩展格的积分解表明，只要满足 iEx-逻辑的公理，在这一组合逻辑中的推理可以分解为分别在直觉主义和正交模态组件中进行推理。
3. 模态鲁棒性： 向模态算子的扩展表明，该代数方法足以处理模态，前提是满足特定的约束（如 Fischer Servi 代数和 DOM 代数中的约束），以确保在嵌入过程中保持模态算子。

作者最后列出了开放性问题，包括 iEx-逻辑的计算复杂度、所提公理的独立性，以及寻找具有有限变量数的有限公理化方案。他们明确指出，构造性量子模态逻辑的研究属于未来的工作，并指出目前的模态结果依赖于特定的代数限制，以克服在商映射中保持模态算子的困难。