模态伙伴

在逻辑中，中间(超直觉)逻辑 L 的模态伙伴是通过下面的特定规范变换解释 L 的正规模态逻辑。模态伙伴共享最初中间逻辑的各种性质，这确使使用为模态逻辑开发的工具研究中间逻辑。

哥德尔–McKinsey–塔斯基变换
设 A 是命题直觉公式。模态公式 T(A)通过在 A 的复杂性上的归纳来定义:
:T(p)=\Box p 对于任何命题变量 p，
:T(\bot)=\bot，
:T(A\land B)=T(A)\land T(B)，
:T(A\lor B)=T(A)\lor T(B)，
:T(A\to B)=\Box(T(A)\to T(B))。
直觉逻辑中的否定定义为 A\to\bot，我们还有
:T(\neg A)=\Box\neg T(A)。
T 叫做哥德尔变换或哥德尔–McKinsey–塔斯基变换。这个变换有时以稍微不同的方式来定义: 例如，我们可以在所有子公式前插入 \Box。所有变体都被证明在 S4 中等价。

模态伙伴
对于扩展 S4 的任何正规模态逻辑 M，我们定义它的 si-片段 ρM 为
:\rho M=\{A;\,M\vdash T(A)\}。
任何 S4 的正规扩展的 si-片段是中间逻辑。模态逻辑 M 是中间逻辑 L 的模态伙伴，如果 L=\rho M。

所有中间逻辑都有模态伙伴。L 的最小模态伙伴是
:\tau L=\mathbf{S4}+\{T(A);\,L\vdash A\}，
这里的 + 指示正规闭包。可以证实所有中间逻辑还有最大模态伙伴，它指示为 σL。模态逻辑 M 是 L 的伙伴，当且仅当 \tau L\subseteq M\subseteq\sigma L。

例如，S4 自身是直觉逻辑(IPC)的最小模态伙伴。IPC 的最大模态伙伴是 Grzegorczyk 逻辑 Grz，公理化自在 K 上的公理
:\Box(\Box(A\to\Box A)\to A)\to A。
经典模态逻辑(CPC)的最小模态伙伴是 Lewis 的 S5，而它的最大模态伙伴是逻辑
:\mathbf{Triv}=\mathbf K+A\equiv\Box A。
更多的例子:

Blok–Esakia 同构
中间逻辑 L 的扩展的集合按包含排序形成了一个完全格，指示为 ExtL。类似的模态逻辑 M 的正规扩展的集合形成了完全格 NExtM。伙伴算子 ρM、τL 和 σL 可以被认为是在格 ExtIPC 和 NExtS4 之间的映射:
:\rho\colon\mathrm{NExt}\,\mathbf{S4}\to\mathrm{Ext}\,\mathbf{IPC}，
:\tau,\sigma\colon\mathrm{Ext}\,\mathbf{IPC}\to\mathrm{NExt}\,\mathbf{S4}。
容易看出所有这三个都是单调的，并且 \rho\circ\tau=\rho\circ\sigma 是在 ExtIPC 上的恒等函数。L. Maximova 和 V. Rybakov 已经证明了 ρ、τ 和 σ 实际上是完全格同态。模态伙伴理论基石是 Blok–Esakia 定理，由 Wim Blok 和 Leo Esakia 独立证明。它声称
:映射 ρ 和 σ 是 ExtIPC 和 NExtGrz 之间的互逆格同构。
因此，σ 与 ρ 受 NExtGrz 的限制叫做 Blok–Esakia 同构。Blok–Esakia 定理的一个重要推论是最大伙伴的简单语法描述: 对于所有中间逻辑 L，
:\sigma L=\tau L+\mathbf{Grz}。

语义描述
哥德尔变换有框架理论对应者。设 \mathbf F=\langle F,R,V\rangle 是自反传递模态一般框架，预序 R 引发在 F 上的等价关系
:x\sim y \iff x\,R\,y \land y\,R\,x，

它的等同点属于同一个簇(cluster)。设 \langle\rho F,\le\rangle=\langle F,R\rangle/{\sim} 是引发的商偏序 (就是说 ρF 是 \sim 的等价类的集合)，并置
:\rho V=\{A/{\sim};\,A\in V,A=\Box A\}。
则 \rho\mathbf F=\langle\rho F,\le,\rho V\rangle 是直觉一般框架，叫做 F 的骨架(skeleton)。骨架构造的点是那些保持有效模哥德尔变换的点: 对于任何直觉公式 A，
:A 在 ρF 中是有效的，当且仅当 T(A) 在 F 中是有效的。
所以模态逻辑 M 的 si-片段可以语义上定义为: 如果 M 关于传递自反一般框架的类 C 是完备的，则 ρM 关于类 \{\rho\mathbf F;\,\mathbf F\in C\} 是完备的。

最大模态伙伴也有语义描述。对于任何直觉一般框架 \mathbf F=\langle F,\le,V\rangle，设 σV 是 V 在布尔运算下的闭包(二元交集和补集)。可以证明 σV 闭合在 \Box 下，所以 \sigma\mathbf F=\langle F,\le,\sigma V\rangle 是一般模态框架。σF 的骨架同构于 F。如果 L 是关于一般框架的类 C 是完备的，则它的最大模态伙伴 σL 关于 \{\sigma\mathbf F;\,\mathbf F\in C\} 是完备的。
Kripke框架的骨架自身是 Kripke 框架。换句话说，σF 永远不是 Kripke 框架，如果 F 是无限深度的 Kripke 框架。

保持定理
模态伙伴和 Blok–Esakia 定理作为研究中间逻辑的工具的价值来自逻辑的很多有趣的性质被某些或全部映射 ρ、σ 和 τ 所保持。例如：
*可判定性被 ρ、τ 和 σ 保持，
*有限模型性质被 ρ、τ 和 σ 保持，
*表格性被 ρ 和 σ 保持，
*Kripke完备性被 ρ 和 τ 保持，
*Kripke 框架上的一阶可定义性被 ρ 和 τ 保持。

其他性质
所有自洽中间逻辑 L 都有无限数目个模态伙伴，此外 L 的模态伙伴集合 \rho^{-1}(L) 包含无穷降链。例如，\rho^{-1}(\mathbf{CPC}) 构成自 S5 和逻辑 L(C_n) 对于所有正整数 n，这里的 C_n 是 n-元素簇。任何 L 的模态伙伴的集合要么是可数的，要么有连续统的势。Rybakov 已经证明了格 ExtL 可以嵌入 \rho^{-1}(L) 中，特别是，一个逻辑有连续统个模态伙伴，如果它有连续统个扩展(比如这杜宇在 KC 之下的所有中间逻辑成立)。它的逆命题是否成立仍未知。

哥德尔变换可以应用于规则同公式一样: 规则
:R=\frac{A_1,\dots,A_n}{B}
的变换是规则
:T(R)=\frac{T(A_1),\dots,T(A_n)}{T(B)}。
规则 R 在逻辑 L 中是可接纳性的，如果 L 的定理的集合闭合在 R 下。容易看出 R 在中间逻辑 L 中是可接纳性的，只要 T(R) 在 L 的模态伙伴中是可接纳性的。逆命题一般不为真，但是对于 L 的最大模态伙伴成立。

引用
Alexander Chagrov and Michael Zakharyaschev, Modal Logic*, vol. 35 of Oxford Logic Guides, Oxford University Press, 1997.
Vladimir V. Rybakov, Admissibility of Logical Inference Rules*, vol. 136 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1997.