[科普中國]-模態(tài)伙伴

在邏輯中，中間(超直覺)邏輯 L 的模態(tài)伙伴是通過下面的特定規(guī)范變換解釋 L 的正規(guī)模態(tài)邏輯。模態(tài)伙伴共享最初中間邏輯的各種性質(zhì)，這確使使用為模態(tài)邏輯開發(fā)的工具研究中間邏輯。

定義對于擴展S4的任何正規(guī)模態(tài)邏輯M，我們定義它的si-片段ρM為1

任何S4的正規(guī)擴展的 si-片段是中間邏輯。模態(tài)邏輯M是中間邏輯L的模態(tài)伙伴，如果 。

所有中間邏輯都有模態(tài)伙伴。L的最小模態(tài)伙伴是

這里的 + 指示正規(guī)閉包。可以證實所有中間邏輯還有最大模態(tài)伙伴，它指示為 σL。模態(tài)邏輯M是L的伙伴，當且僅當。

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

經(jīng)典模態(tài)邏輯(CPC)的最小模態(tài)伙伴是 Lewis 的S5，而它的最大模態(tài)伙伴是邏輯

更多的例子:

|| ||

語義描述哥德爾變換有框架理論對應者。設是自反傳遞模態(tài)一般框架，預序R引發(fā)在F上的等價關系

它的等同點屬于同一個簇(cluster)。設是引發(fā)的商偏序，并置2

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

A在 ρF中是有效的，當且僅當T(A) 在F中是有效的。

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

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

可判定性被 ρ、τ 和 σ 保持，

有限模型性質(zhì)被 ρ、τ 和 σ 保持，

表格性被 ρ 和 σ 保持，

Kripke完備性被 ρ 和 τ 保持，

Kripke 框架上的一階可定義性被 ρ 和 τ 保持。

性質(zhì)所有自洽中間邏輯L都有無限數(shù)目個模態(tài)伙伴，此外L的模態(tài)伙伴集合包含無窮降鏈。

哥德爾變換可以應用于規(guī)則同公式一樣: 規(guī)則

的變換是規(guī)則

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

本詞條內(nèi)容貢獻者為:

李嘉騫 - 博士 - 同濟大學