模态同伴

在逻辑学中，超直觉（中间）逻辑L的模态同伴是一种正常的模态逻辑，它通过某种典范的转换来解释L，描述如下。模态同伴共享原始中间逻辑的各种属性，这使得我们能够使用为模态逻辑开发的工具来研究中间逻辑。

哥德尔-麦 -塔斯基翻译让A是一个命题直观公式。一个模态公式T(A)是通过对A的复杂性的归纳来定义的。对于任何命题变量T被称为哥德尔翻译或哥德尔-麦 -塔尔斯基翻译。该翻译有时会以稍微不同的方式呈现：例如，人们可以插入◻{displaystyle{Box}在每个子公式之前。所有这些变体在S4中都是可证明的等价物。

模态同伴对于任何扩展了S4的正常模态逻辑M，我们将其si-fragmentρM定义为ρM={A∣M⊢T(A)}.{displaystylerhoM={AmidMvdashT(A)}。S4的任何正常扩展的si-fragment是一个超直觉的逻辑。一个模态逻辑M是一个超直觉逻辑L的模态同伴，如果每个超直觉逻辑都有模态同伴。L的最小的模态同伴是{displaystyleoplus}表示法线闭合。表示法线闭合。可以证明，每个超直觉逻辑也有一个xxx的模态同伴，用σL表示。

一个模态逻辑M是L的一个同伴，当且仅当例如，S4本身就是直觉逻辑（IPC）最小的模态伴生物。

IPCxxx的模态伙伴是Grzegorczyk逻辑Grz，其公理为古典逻辑（CPC）最小的模态同伴是刘易斯的S5，而它xxx的模态同伴是逻辑

超直觉逻辑L的扩展集按包含性排序，形成一个完整的网格，表示为ExtL。类似地，模态逻辑M的正常扩展集是一个完整的格子NExtM。伴生算子ρM、τL和σL可以被看作是格子ExtIPC和NExtS4之间的映射。{displaystylerhocirctau=rhocircsigma}是ExtIPC上的同一函数。是ExtIPC上的身份函数。L.Maksimova和V.Rybakov已经证明，ρ、τ和σ实际上分别是完全、连接完全和满足完全的格子同构。

模态同伴理论的基石是Blok-Esakia定理，由WimBlok和LeoEsakia独立证明。它指出映射ρ和σ是ExtIPC和NExtGrz的相互逆格子同构。因此，σ和ρ对NExtGrz的限制被称为Blok-Esakia同构。Blok-Esakia定理的一个重要推论是对xxx模态同伴的简单句法描述：对于每个超直觉逻辑L。

哥德尔翻译有一个框架理论的对应物。让{displaystylemathbf{F}=langleF,R,Vrangle}是一个传递性和反射性的框架。是一个传递性和反射性的模态一般框架。