模態夥伴

在邏輯中，中間(超直覺)邏輯 L 的模態夥伴是通過下面的特定規範變換解釋 L 的正規模態邏輯。模態夥伴共享最國中間邏輯的各種性質，這確使使用為模態邏輯開發的工具研究中間邏輯。

定義

對於擴展S4的任何正規模態邏輯M，我們定義它的si-片段ρM為

任何S4的正規擴展的 si-片段是中間邏輯。模態邏輯M是中間邏輯L的模態夥伴，如果 。

所有中間邏輯都有模態夥伴。L的最小模態夥伴是

這裡的 + 指示正規閉包。可以證實所有中間邏輯還有最大模態夥伴，它指示為 σL。模態邏輯M是L的夥伴，若且唯若。

例如，S4自身是直覺邏輯(IPC)的最小模態夥伴。IPC的最大模態夥伴是Grzegorczyk邏輯Grz，公理化自在K上的公理

經典模態邏輯(CPC)的最小模態夥伴是 Lewis 的S5，而它的最大模態夥伴是邏輯

更多的例子:

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	見後

語義描述

哥德爾變換有框架理論對應者。設是自反傳遞模態一般框架，預序R引發在F上的等價關係

它的等同點屬於同一個簇(cluster)。設是引發的商偏序，並置

則是直覺一般框架，叫做F的骨架(skeleton)。骨架構造的點是那些保持有效模哥德爾變換的點: 對於任何直覺公式A，

• A在 ρF中是有效的，若且唯若T(A) 在F中是有效的。
  

所以模態邏輯M的 si-片段可以語義上定義為: 如果M關於傳遞自反一般框架的類C是完備的，則 ρM關於類是完備的。

保持定理

模態夥伴和 Blok–Esakia 定理作為研究中間邏輯的工具的價值來自邏輯的很多有趣的性質被某些或全部映射 ρ、σ 和 τ 所保持。例如：

• 可判定性被 ρ、τ 和 σ 保持，
  
• 有限模型性質被 ρ、τ 和 σ 保持，
  
• 表格性被 ρ 和 σ 保持，
  
• Kripke完備性被 ρ 和 τ 保持，
  
• Kripke 框架上的一階可定義性被 ρ 和 τ 保持。
  

性質

所有自洽中間邏輯L都有無限數目個模態夥伴，此外L的模態夥伴集合包含無窮降鏈。

哥德爾變換可以套用於規則同公式一樣: 規則

的變換是規則

規則R在邏輯L中是可接納性的，如果L的定理的集合閉合在R下。容易看出R在中間邏輯L中是可接納性的，只要T(R) 在L的模態夥伴中是可接納性的。逆命題一般不為真，但是對於L的最大模態夥伴成立。