查看“模态伙伴”的源代码

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

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

==模态伙伴==

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

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

例如，'''S4''' 自身是直觉逻辑('''IPC''')的最小模态伙伴。'''IPC''' 的最大模态伙伴是 [[Andrzej Grzegorczyk|Grzegorczyk]] 逻辑 '''Grz'''，公理化自在 '''K''' 上的公理
:<math>\Box(\Box(A\to\Box A)\to A)\to A</math>。
经典模态逻辑('''CPC''')的最小模态伙伴是 Lewis 的 '''S5'''，而它的最大模态伙伴是逻辑
:<math>\mathbf{Triv}=\mathbf K+A\equiv\Box A</math>。
更多的例子:
{|  class="wikitable"
|''L''
|&tau;''L''
|&sigma;''L''
|''L'' 的其他伙伴
|-
|'''IPC'''
|'''S4'''
|'''Grz'''
|'''S4.1''', '''Dum''', ...
|-
|'''KC'''
|'''S4.2'''
|'''Grz.2'''
|'''S4.1.2''', ...
|-
|'''LC'''
|'''S4.3'''
|'''Grz.3'''
|'''S4.1.3''', '''S4.3Dum''', ...
|-
|'''CPC'''
|'''S5'''
|'''Triv'''
|见后
|-
|}

==Blok–Esakia 同构==

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

==语义描述==

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

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

==保持定理==

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

==其他性质==

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

哥德尔变换可以应用于[[推理规则|规则]]同公式一样: 规则
:<math>R=\frac{A_1,\dots,A_n}{B}</math>
的变换是规则
:<math>T(R)=\frac{T(A_1),\dots,T(A_n)}{T(B)}</math>。
规则 ''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.

[[Category:模态逻辑]]