模态伙伴

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

Gödel–McKinsey–Tarski 变换

设 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}$。

语义描述

已隱藏部分未翻譯内容，歡迎參與翻譯。

The Gödel translation has a frame-theoretic counterpart. Let $\mathbf {F} =\langle F,R,V\rangle$ be a transitive and reflexive modal general frame. The preorder R induces the equivalence relation

$x\sim y\iff x\,R\,y\land y\,R\,x$

on F, which identifies points belonging to the same cluster. Let $\langle \rho F,\leq \rangle =\langle F,R\rangle /{\sim }$ be the induced quotient partial order (i.e., ρF is the set of equivalence classes of $\sim$), and put

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

Then $\rho \mathbf {F} =\langle \rho F,\leq ,\rho V\rangle$ is an intuitionistic general frame, called the skeleton of F. The point of the skeleton construction is that it preserves validity modulo Gödel translation: for any intuitionistic formula A,

A is valid in ρF if and only if T(A) is valid in F.

Therefore the si-fragment of a modal logic M can be defined semantically: if M is complete with respect to a class C of transitive reflexive general frames, then ρM is complete with respect to the class $\{\rho \mathbf {F} ;\,\mathbf {F} \in C\}$.

The largest modal companions also have a semantic description. For any intuitionistic general frame $\mathbf {F} =\langle F,\leq ,V\rangle$, let σV be the closure of V under Boolean operations (binary intersection and complement). It can be shown that σV is closed under $\Box$, thus $\sigma \mathbf {F} =\langle F,\leq ,\sigma V\rangle$ is a general modal frame. The skeleton of σF is isomorphic to F. If L is an intermediate logic complete with respect to a class C of general frames, then its largest modal companion σL is complete with respect to $\{\sigma \mathbf {F} ;\,\mathbf {F} \in C\}$.

The skeleton of a Kripke frame is itself a Kripke frame. On the other hand, σF is never a Kripke frame if F is a Kripke frame of infinite depth.

保持定理

已隱藏部分未翻譯内容，歡迎參與翻譯。

The value of modal companions and the Blok–Esakia theorem as a tool for investigation of intermediate logics comes from the fact that many interesting properties of logics are preserved by some or all of the mappings ρ, σ, and τ. For example,

• decidability is preserved by ρ, τ, and σ,
• finite model property is preserved by ρ, τ, and σ,
• tabularity is preserved by ρ and σ,
• Kripke completeness is preserved by ρ and τ,
• first-order definability on Kripke frames is preserved by ρ and τ.

其他性质

已隱藏部分未翻譯内容，歡迎參與翻譯。

Every consistent intermediate logic L has an infinite number of modal companions, and moreover, the set $\rho ^{-1}(L)$ of modal companions of L contains an infinite descending chain. For example, $\rho ^{-1}(\mathbf {CPC} )$ consists of S5, and the logics $L(C_{n})$ for every positive integer n, where $C_{n}$ is the n-element cluster. The set of modal companions of any L is either countable, or it has the cardinality of the continuum. Rybakov has shown that the lattice ExtL can be embedded in $\rho ^{-1}(L)$; in particular, a logic has a continuum of modal companions if it has a continuum of extensions (this holds, for instance, for all intermediate logics below KC). It is unknown whether the converse is also true.

The Gödel translation can be applied to rules as well as formulas: the translation of a rule

$R={\frac {A_{1},\dots ,A_{n}}{B}}$

is the rule

$T(R)={\frac {T(A_{1}),\dots ,T(A_{n})}{T(B)}}.$

A rule R is admissible in a logic L if the set of theorems of L is closed under R. It is easy to see that R is admissible in an intermediate logic L whenever T(R) is admissible in a modal companion of L. The converse is not true in general, but it holds for the largest modal companion of 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.