Possibly Relevant Translations

技术摘要：可能的关联翻译

问题与动机
本文探讨了相关逻辑（特别是 Anderson–Belnap 系谱）与正规模态逻辑之间的结构关系。虽然直觉主义逻辑向经典模态逻辑的翻译（通过 Gödel–McKinsey–Tarski 翻译）在历史上促进了显著的跨传统交流，但相关逻辑与模态逻辑之间类似的系统性翻译仍处于发展不足的状态。作者旨在建立从相关逻辑到正规模态逻辑的全保真（full and faithful）翻译，以阐明结构联系、推导推论结果，并识别当前翻译方法的局限性。本研究最初侧重于正向片段 $\{\land, \lor, \to\}$，并逐渐扩展到包含真常数 $t$、融合算子 $\circ$ 以及否定 $\neg$。

方法论
本文采用语义方法，利用两个不同框架之间的模型转换：

1. Routley–Meyer 框架： 相关逻辑的标准语义，定义为三元组 $(K, R, N)$，其中 $R$ 是一个三元关系，$N$ 是一组正向点，并受特定的顺序和关系约束（例如“下-下-上”条件）。
2. Kripke 框架： 正规模态逻辑的标准语义，定义为二元组 $(W, R)$（或对于扩展语言带有附加关系的元组）。

核心方法论涉及定义一个从相关公式到模态公式的翻译函数（记作 $\star, \ast$ 或 $\circ$）。为了证明这些翻译是全保真的（即如果一个相关蕴含成立，则其模态翻译也成立）且是忠实的（即如果其模态翻译成立，则相关蕴含也成立），作者构建了两个模型转换：

• $F$：将指向型 Kripke 模型映射到指向型 Routley–Meyer 模型。
• $G$：将指向型 Routley–Meyer 模型映射到指向型 Kripke 模型。

这些转换旨在满足伴随模式（adjunction patterns），使得在一个模型中的满足对应于在另一个模型中翻译后公式的满足。论文还利用对应理论（特别是 Sahlqvist 对应）来识别 Kripke 语义中对应于特定相关公理的框架条件。

主要贡献与结果

1. 基础正向翻译 ($\star$)：

   • 作者为 $\{\land, \lor, \to\}$ 片段定义了翻译 $\star$，其中 $\to$ 被映射为一个定义的模态算子 $\neg \Diamond(\cdot, \neg \cdot)$。
   • 定理 1.4： 确立了对于基础相关逻辑 $B^+$ 和基础二元模态逻辑 $K_2$，$\vdash_{B^+} \phi \to \psi$ 当且仅当 $\vdash_{K_2} \phi^\star \supset \psi^\star$。
   • 向更强逻辑的扩展： 该翻译扩展到由公理 7–10 的子集（如 $TW^+, TWJ^+, C^+$）公理化的逻辑。然而，论文表明该翻译对于需要收缩（axiom 11）或断言（axiom 12）的逻辑（如 $R^+$）失效。这种失效源于较简单的 Kripke 语义缺乏 Routley–Meyer 框架中固有的特定顺序条件（如“下-下-上”属性），而这些条件对于验证这些公理是必要的。

2. 嵌套蕴含翻译 ($\ast$)：

   • 为了处理主联结词不是 $\to$ 的公式，引入了第二个翻译 $\ast$，将 $\phi \to \psi$ 映射为 $\Box_\to(\phi^\star \supset \psi^\star)$。
   • 定理 1.7： 表明 $\ast$ 为 $B^+$ 到 $K_2$ 提供了全保真嵌入，将 $B^+$ 实现为 $K_2$ 的句法片段。
   • 与 $\star$-翻译类似，该方法在扩展到涉及收缩和断言的逻辑时也会遇到限制。

3. 不可判定性与插值性：

   • 本文将相关逻辑的不可判定性结果转移到模态逻辑中。具体而言，它证明了对应于 $TWJ^+$ 和 $C^+$ 框架条件的模态逻辑是不可判定的（定理 1.9），补充了 Urquhart 及其他人的现有结果。
   • 作者提出了关于 Craig 插值性质（CIP）的开放性问题。虽然 $K_2$ 具有 CIP，但目前尚不清楚 $B^+$ 是否具有。该翻译表明，如果 $B^+$ 缺乏 CIP，可能是由于特定翻译的行为或词汇量的缺乏。

4. 扩展翻译 ($\circ$)：

   • 为了克服先前翻译在处理收缩和断言方面的局限性，论文引入了一种进入更丰富模态语言的翻译，该语言包含一个零元模态 $t$ 和一个二元模态 $\circ$。
   • 定义 2.2： 将模态 $B^+$ ($Mod.B^+$) 定义为包含剩余公理（residuation axioms）以及对应于 Routley–Meyer 框架条件（自反性、传递性、上集等）的最小正规模态逻辑。
   • 定理 2.5： 表明对于扩展了 $t$ 和 $\circ$ 的语言，翻译 $\circ$ 是全保真的：$\vdash_B \phi$ 当且仅当 $\vdash_{Mod.B^+} t \supset \phi^\circ$。该翻译成功地在 Kripke 语义中捕捉了 Routley–Meyer 框架的结构约束（包括顺序关系 $\leq$）。
   • 定理 2.8： 通过引入一元模态 $\Box_\neg$ 和相应的框架条件（对合性与顺序反转），将此结果扩展到包含否定 $\neg$ 的全语言。

意义与主张
本文谦虚地声称通过一系列翻译澄清了相关逻辑与模态逻辑之间的结构联系。其主要意义在于：

• 提供了基础相关逻辑 $B$（及其通过 $t, \circ, \neg$ 进行的扩展）到特定正规模态逻辑 ($Mod.B$) 的全保真翻译，从而将相关逻辑实现为模态逻辑的一个句法片段。
• 强调了较简单翻译（如 $\star$）在应用于更强相关逻辑（如 $R^+$）时的局限性，特别指出标准的 Kripke 框架在没有额外公理或模态的情况下，无法捕捉 Routley–Meyer 框架中必要的顺序论属性。
• 促进了两种传统之间元逻辑属性（如可判定性与不可判定性）的转移。
• 确定了未来的开放性问题，特别是关于 $B^+$ 中的插值性质，以及深化其结构联系以包含框架不完备逻辑的可能性。

作者明确指出，本文是“探索性的、广泛的而非深入的”，将更充分的哲学动机分析和更深层的结构关系留给未来的工作。