模態夥伴

在邏輯中，中間(超直覺)邏輯 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$。

更多的例子:

L	τL	σ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 的擴展的集合按包含排序形成了一個完全格，指示為 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,\leq \rangle =\langle F,R\rangle /{\sim }$ 是引發的商偏序 (就是說 ρF 是 $\sim$ 的等價類的集合)，並置

$\rho V=\{A/{\sim };\,A\in V,A=\Box A\}$。

則 $\rho \mathbf {F} =\langle \rho F,\leq ,\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,\leq ,V\rangle$，設 σV 是 V 在布爾運算下的閉包(二元交集和補集)。可以證明 σV 閉合在 $\Box$ 下，所以 $\sigma \mathbf {F} =\langle F,\leq ,\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.