现代模态逻辑

第三节　现代模态逻辑

现代模态逻辑是在数理逻辑的推动下产生和发展起来的，可分为模态命题逻辑和模态谓词逻辑两种类型。限于篇幅和本书的性质，本节仅对作为基础的模态命题逻辑做简单介绍。

一、命题逻辑基础

现代模态逻辑可以说是命题逻辑加上一个模态算子的扩张，所以首先应对命题逻辑的基本内容有一个简单了解。

命题逻辑是现代逻辑的基础部分。它仍然是以简单命题(即判断)为单位，研究命题经逻辑联结词构成的复合命题的逻辑性质以及关于复合命题之间的推理关系。与传统逻辑不同的是，现代逻辑使用的是人工语言，采用完全公理化的方法，把命题之间的推理关系作为一个形式系统的命题演算加以处理。一个形式系统通常是由四部分组成的:(1)作为出发点的各种初始符号。初始符号是一个形式系统使用的符号，如p、q、r……以及前面提到的逻辑联结词等。这些符号经解释后一部分可称为初始概念，如命题演算中的“∨”是一个初始符号，经解释后它表示“析取”。(2)规定初始符号如何构成合式公式的一组形成规则。初始符号可以组成不同的符号序列。形成规则规定，哪些符号序列是需要研究的，因为这类符号序列经解释后是有意义的命题，称之为合式公式，简称公式。例如，在命题演算中，“∨pq”是没有意义的符号序列，而“p∨q”的组合则是一个合式公式，它表示一个析取命题。(3)作为演绎出发点的公式，即“公理”。形式系统建立的目的是要把所有的重言式(即永真式)汇集成一个整体。在这个整体中，重言式能演绎地排列出来，而且排在后面的总可以从前面推出。公理可以推出其他“重言式”，并且都是形式系统中的公式。(4)充当演绎角色的“推理规则”。推理规则规定如何从一个公式或一组公式通过符号变换得出另一个公式，由推理规则推导出的公式叫做这个系统的定理。总之，一个形式系统是由它的符号、公式、公理和推理规则完全确定的，形式系统可以看做一个完全形式化了的公理系统。所谓公理系统，就是从一些叫做公理的公式出发，根据演绎规则，推导出一系列叫做定理的公式，这样形成的演绎体系就叫做公理系统。命题逻辑的重言式组成的系统就是一个公理系统。

另外，由于所建立的符号语言是纯形式的，使用的是特定的人工语言，也属于一种表意的符号语言，这就需要使符号与其所要表达的意义之间有完全的对应。因此，在讲到概念、判断和推理时，就可以用与它们相应的符号、公式，从而使对判断的研究转化为对形式语言的研究，即对这种语言的语法和语义问题的研究。由于，命题演算作为形式系统必须要经过解释后才能有意义，才能成为关于某一领域的真正的公理系统。所以，对语言符号规定一种解释，就属于命题演算的语义研究。

下面，我们就以公理系统P为例进行具体分析。

二、命题演算的公理系统P

形式系统使用的语言是形式语言，相对于自然语言来说，具有严格、精确的特点，可以避免自然语言的种种歧异。下面对系统P的分析是从形式语言开始，一般记为L_p。

(一)形式语言L_O

1．L_p的初始符号

甲类:p，q，r，s，p₁，q₁，r₁，s₁，p₂，…;

乙类:﹁，∨;

丙类:(，)。

初始符号相当于自然语言中的字母。形式语言L_O实际上由可数无穷多个符号组成，即

L_O={﹁，∨，(，)，p，q，r，s，p₁，q₁，r₁，s₁，p₂，…}

其中，甲类符号表示命题变项;乙类符号表示真值联结词，其中“﹁”表示否定，“∨”表示析取;丙类符号是技术符号，左右括号可对符号序列进行分组，规定运算的次序。

2．L_O的形成规则

甲:任一甲类符号是一合式公式;

乙:如果符号序列X是合式公式，则﹁X也是合式公式;

丙:如果符号序列X和Y都是合式公式，则X∨Y也是合式公式;

丁:只有适合以上三条的符号序列才是合式公式，简称为公式，记做W_ff。

3.定义

定义甲　α∧β定义为﹁(﹁α∨﹁β)。

定义乙　α→β定义为(﹁α∨β)。

定义丙　(α→β)定义为((α→β)∧(β→α))。

(二)演绎工具

1．P的公理模式

A₁:α∨α→α;　A₂:α→α∨β;

A₃:α∨β→β∨α;　A₄:(β→γ)→((α∨β)→(α∨γ))。

A₁至A₄是四个公理模式，每个模式都代表着无穷多条公理。A₁被称为“重言律”。A₂的意思是，“如果α是真的，那么α或者β也是真的”。由于前件没有析取词而后件引入了析取词，所以A₂又被称为“析取引入律”。A₃被称为“析取交换律”。A₄被称为“析取附加律”。

下面给出从公理得到定理的推理工具，即“推理规则”。

2．P的推理规则

(1)分离规则:由α和α→β可推出β。

这条推理规则的含义:如果α和α→β被断定，那么β也被断定，即从α和α→β可得β。这是承认前件的假言推理，记做MP(Modus Ponens)规则。

(2)代入规则:公式α中出现的某一甲类符号，可以用公式β代入或者替换。

只有甲类符号可以代入，若某一甲类符号在公式中多次出现，只能全部用同一公式进行代入。

由公理和推理规则可以构成一个无穷集合，这个无穷集合包括两类:第一类是公理;第二类是由公理根据推理规则推出的定理。这一集合可以说是本系统所有重言式的汇集，即公理系统P的定理集。

(三)定理

在公理和推理规则给定之后，根据这些公理和推理规则能够将其余的“重言式”推导出来。这个演绎的过程也叫证明。严格地说，满足下面两个条件之一的公式所组成的有穷公式序列称为本系统的一个证明:

(1)是公理之一;

(2)是由序列中排在前面的两个公式运用MP规则得到的。

证明的有穷公式序列的最后一个公式记做α，并称该证明是公式α的一个证明，或者说α是可证的，记作├α，表明α是本系统的一个定理。

下面是4个定理的详细证明:

定理1　(β→γ)→((α→β)→(α→γ))

证明:

①(β→γ)→((α∨β)→(α∨γ))　　　(A₄)

②(β→γ)→((﹁α∨β)→(﹁α∨γ))　(①，代入规则)

③(β→γ)→((α→β)→(α→γ))　　　(②，定义置换)

定理2　α→α

证明:

①α→α∨β　　(A₂)

②α→α∨α　　(①，代入规则)

③α∨α→α　　(A₁)

④(β→γ)→((α→β)→(α→γ))　　(定理1)

⑤(α∨α→α)→((α→α∨α)→(α→α))　　(④，代入规则)

⑥(α→α∨α)→(α→α)　　(③，⑤，MP)

⑦α→α　　(②，⑥，MP)

定理3　﹁α∨α

证明:

①α→α　　(定理2)

②﹁α∨α　　(①，定义置换)

定理4α∨﹁α

证明:

①﹁α∨α→α∨﹁α　　(A₃)

②﹁α∨α　　(定理3)

③α∨﹁α　　(①，②，MP)

定理5　α→﹁﹁α

定理6　﹁﹁α→α

定理7　(α→β)→(﹁β→﹁α)

定理8　(﹁β→﹁α)→(α→β)

定理9　(α∧β)→﹁α∨﹁β

定理10　﹁α∨﹁β→(α∧β)

定理11　α→β∨α

当然，这个系统的可证定理还有很多，不再一一列举。从以上定理的证明可以看出:依照定义而写出的证明有时过于冗长，在实际操作中可以根据已证定理和推理规则进行简化证明。简化过的结果称为系统PC的导出规则。P的常用导出规则还有:

(三段论规则)├β→γ和├α→β，可得├α→γ。

(合取分解)若├α∧β，则├α;若├α∧β，则├β。

(条件合取)若├α→β→γ，则├α∧β→γ。

(等值构成)若├α→β和├β→α则├α→β。

(等值置换)若├β→γ，则├α→α［β/γ］或若├β→γ和├α，则├α［β/γ］。

(假言易位)若├α→β，则├﹁β→﹁α。

上述公理系统具有完全性和一致性，即这个公理系统能够推导出该系统中的所有重言式，并且不会推演出逻辑矛盾，证明从略。

三、现代模态逻辑的内容和特点

经典命题演算的建立，促进了现代逻辑的迅速发展。但命题演算系统中有一些关于实质蕴涵的定理，却与日常的理解相悖。比如:﹁α→(α→β)、α→(β→α)，它们分别表明“假命题蕴涵任何命题”，以及“真命题为任何命题所蕴涵”，这就是命题逻辑中的实质蕴涵悖论。并且，系统中还存在着很多类似的定理。由于蕴涵悖论与日常思维中的蕴涵关系相背离，美国逻辑学家刘易斯(C.I.Lewis)提出了不同于实质蕴涵的严格蕴涵，希望能够建立反映日常蕴涵关系的逻辑系统。于是，他以经典命题演算为基础，构造了一系列严格蕴涵系统，标志着现代模态逻辑的产生。目前，模态逻辑已经发展成为非经典逻辑中最成熟的分支，并在它的基础上衍生出一系列广义模态逻辑分支。

现代模态逻辑的主要特点表现为以下几个方面:

第一，它以逻辑的模态为主要研究对象，并由此扩展到其他的模态;

第二，它是形式化和公理化的，表现为建立一些模态的公理系统;

第三，它仍然是以经典逻辑为基础，是经典逻辑加一个模态算子的扩张;

第四，在研究上注重语形与语义的结合，不但建立形式系统，而且给出语义解释;

第五，它扩展了现代逻辑的研究范围，在狭义模态逻辑的基础上延伸出一大批广义模态逻辑分支，如规范逻辑、时态逻辑、认知逻辑等。

因此，现代模态逻辑的建立，极大地推动了现代逻辑的繁荣和发展，其研究方法和研究成果对哲学、法学、计算机和信息科学等很多相关领域的发展也有重要的理论意义和实践价值。

(一)模态命题逻辑系统L_PM

模态命题逻辑系统L_PM是在命题演算的公理系统P的基础上，增加必然模态算子“□”的扩张，属于最基本的模态命题逻辑系统。

1.模态命题逻辑语言L_PM

L_PM是对命题逻辑语言L_P的扩充，L_P中的符号和公式也是L_PM的符号和公式，不过L_PM中增加了模态算子，其公式也随之发生了变化。

I.初始符号

在L_P初始符号基础上增加:

丁:□;

其中，甲、乙、丙类符号与命题逻辑相同，丁类符号“□”为模态算子，表示“必然”。

II.定义符号

在L_P定义基础上增加:

定义丁:◇α=_df﹁□﹁α

说明:◇是模态算子，表示“可能”。◇可以通过□进行定义。需注意的是，也可以选择◇作为初始算子来定义□，二者可以相互定义。

III.形成规则

在L_P形成规则的基础上，增加一条规则:若α是公式，则□α也是公式。

2.系统K

(1)公理

L_P的公理A₁、A₂、A₃、A₄;

A₅:□(α→β)→(□α→□β);

(2)初始规则

MP(分离规则):由α和α→β可推演出β。

SB(代入规则):公式α中出现的某一甲类符号，可以用公式β代入或者替换。

N(必然化规则):由α可推演出□α。

A₁、A₂、A₃、A₄是命题系统P的公理，MP和SB是系统P的初始规则。系统K是在系统P的基础上加上A₅和规则N构成的。所以系统K是对系统P的扩张。

(3)系统K中的定理

Th_K1:□(α→α)

证明:

①(α→α)(P－定理)

②□(α→α)(①，N)

由于系统K是对P的扩张，P中的定理也就是K的定理，在证明过程中可以直接应用。

Th_K2:(□α∧□β)→□(α∧β)

Th_K3:(□α∨□β)→□(α∨β)

(4)系统K的导出规则

导出规则与初始规则一样同属变形规则，但导出规则必须经过证明之后才能使用。因为很多时候仅仅使用初始规则，会使推演和证明过于繁琐。为了追求系统的从简原则，导出规则的使用可以简化推导或证明过程。系统K的导出规则有很多。这里只介绍较为常用的几个:RK、RE□和RK◇。

RK:由α→β推出□α→□β

证明:

①α→β　　(假设)

②□(α→β)　　(①，N)

③□(α→β)→(□α→□β)　　(A₅)

④□α→□β　　(②，③，MP)

RE□:由α→β推出□α→□β

证明:

①α→β　　(假设)

②(α→β)∧(β→α)　　(①，定义(→))

③α→β　　(②，合取分解)

④β→α　　(②，合取分解)

⑤□(α→β)　　(③，N)

⑥□(β→α)　　(④，N)

⑦□α→□β　　(⑤，RK)

⑧□β→□α　　(⑥，RK)

⑨□α→□β　　(⑤，⑥，等值构成)

RK◇:由α→β可推出◇α→◇β

证明:

①α→β　　(假设)

②□(α→β)　　(①，N)

③□(﹁β→﹁α)→(□﹁β→□﹁α)　　(SB(A₅))

④□(α→β)→(﹁□﹁α→﹁□﹁β)　　(等值置换)

⑤﹁□﹁α→﹁□﹁β　　(②，④，MP)

⑥◇α→◇β　　(定义(◇))

Th_K4:□α→﹁◇﹁α

证明:

①α→﹁﹁α　　(P－定理)

②□α→□﹁﹁α　　(①，RE□)

③□α→﹁﹁□﹁﹁α　　(②，等值置换)

④□α→﹁◇﹁α　　(③，定义(◇))

定理Th_K4就是使用了导出规则RE□进行证明的。

Th_K5:□(α∧β)→(□α∧□β)

由Th_K2和Th_K5可以得出下面的定理:

Th_K6:(□α∧□β)→□(α∧β)

系统K其他的定理不再一一列举，可参考周北海的《模态逻辑》，中国社会科学出版社1996年版。

3.对系统K的若干扩张

在一个形式系统S中加进新的公理α，可以推出S中无法证明的定理，从而形成一个新的系统S'，S是S'的真子系统，可以称α是S'的特征公理。下面介绍几个系统K的扩张。

(1)系统D

在系统K中加上公理A₆，就形成了系统D。

A.₆:□α→◇α

D.部分定理和导出规则:

Th_D1:◇(α→α)

Th_D2:(□α∧□β)→◇(α∧β)

导出规则RP:由α可推出◇α。

证明:

①α　　(假设)

②□α　　(①，N)

③□α→◇α　　(A₆)

④◇α　　(②，③，MP)

(2)系统T

在系统K上增加特征公理A₇，就形成了系统T。

A₇:□α→α

系统T的部分定理:

Th_T1:α→◇α

Th_T2:◇(α∧β)→(◇α∧◇β)

Th_T3:□α→◇α

定理Th_T3恰好是系统D的特征公理，因而D－定理也都是T的定理。这表明系统D是系统T的子系统，系统D是系统T的扩张。

(3)系统S₄和S₅

模态系统S₄和S₅分别是在T的基础上增加特征公理的扩张:

A₈:□α→□□α

A₉:◇α→□◇α

S₄是在系统T的基础上加进公式A₈得到的，都属于叠置模态。

系统S₄的定理:

Th_S41:□α→□□α

Th_S42:◇◇α→◇α

Th_S43:◇◇α→◇α

Th_S44:◇□◇α→◇α

S₅是在系统T的基础上加进公式A₉得到的。下面给出几个S₅定理。

Th_S51:◇α→□◇α

Th_S52:◇□α→□α

Th_S53:◇□α→□α

Th_S54:□α→□□α

以上简要介绍了模态系统K、D、T、S₄和S₅，这些系统都是一致的，即不存在公式α，α和﹁α都在系统中可证。系统的一致性，也即是不矛盾性，是对作为逻辑形式系统的最基本的要求之一。

定理1　K是古典一致的，即α与﹁α不能同时为K的定理。

证明:设α是K定理，α'是α的P－变形。因为任一K定理的P－变形都是P定理，所以α'是P定理。由于命题演算P是古典一致的，所以﹁α'不是P定理。由此可得，﹁α不是K定理。

定理2　D、T、S₄、S₅和B都是古典一致的。

证明:与K的证明类似，略。

上面介绍的系统都属于正规系统。所谓正规系统是指命题演算系统P的一种扩张，其中系统K是最小的正规系统。除了正规系统之外，还有其他类型的模态系统，这里从略。

(二)现代模态逻辑语义学

模态系统主要使用形式化的方法刻画模态命题，但它所做的只是形式的推演，对于这样的推演是否有效，仅从模态系统本身无法做出断定。因此，如果不对L_PM－公式做出语义解释，将无法考察模态系统L_PM的另一个基本性质——有效性。模态逻辑的语义学理论也是一个内容非常丰富的领域，这里仅根据本书的需要对模态逻辑的语义学作简单介绍。

在模态逻辑语法研究的推动下，首先发展起来的是模态代数语义学，简称为模态代数。由于模态代数过于数学化而缺少逻辑意义，其抽象的代数内容对于数学基础薄弱的入门者来说较为困难，所以这里不再对它具体描述。另一种随之发展起来的是逻辑语义学，简称语义学，可分为直观语义学和严格语义学。但它对模态的理解上也存在一些困难。在这种背景下，模态代数与逻辑语义学两方面的研究成果相结合，产生了一种新的语义学理论，即可能世界语义学。由于美国哲学家、逻辑学家克里普克(S.A.Kripke)在可能世界语义学的产生过程中贡献较大，也称之为克里普克语义学。可能世界语义学的建立，标志着模态逻辑已经成为现代逻辑的一个重要分支。目前，可能世界语义学被广泛地应用于广义模态逻辑研究中，内容非常丰富，下面主要根据本章的需要对其作为模态逻辑语义学的基础知识予以介绍。

1.可能世界与可及关系

(1)真和可能世界。与命题逻辑不同的是，模态逻辑的表达式包含有模态算子，对模态算子的解释是模态逻辑语义学考察的核心内容。于是在关于模态逻辑语义解释中，不再简单地讨论一个模态命题的真假，而是把模态命题与可能世界结合起来，具体考察模态命题在某个可能世界中的真假。比如，我们不能简单判断命题□α的真假，而是需要考虑它在某个可能世界中的真假。所以，“可能世界”作为可能世界语义学的一个基本概念，必须对它有所了解。

“可能世界”这个概念，最初来源于德国著名数学家、哲学家莱布尼茨(G.W.Leibniz)的思想。他认为存在很多个可能世界，现实世界只是所有可能世界中的一种情况。这里所指的可能世界，既包括物理上的可能世界，也包括逻辑上的可能世界。在现实世界中不可能的情况，也许在某个可能世界中是可能的。比如人会飞檐走壁，在武侠小说这个可能世界中是可能的。具体来说，可能世界是外部世界所有可能情况的总和，也包含着现实世界。因为可能世界有很多，现实世界只是众多可能世界中的一个。简单来说，可能世界就是各种可能的情况，这是最为直观的理解。

根据莱布尼茨的思想，必然性应当在所有可能世界中都是真的，而可能性只需在某个可能世界中是真的。所以，可能世界语义学对模态命题的真假作了如下规定:

①一个必然命题□α在现实世界中是真的，当且仅当，α在所有可能世界里都是真的。

②一个可能命题◇α在某一可能世界中是真的，当且仅当，至少存在一个使得α为真的可能世界。

一般常用w，w₁，w₂，w₃，…表示不同的可能世界，用W，W₁，W₂，…表示可能世界的集合。

(2)可及关系，也称可达关系或可通达关系，是指可能世界之间的某种关系。与可能世界类似，可及关系也有多种理解，比如改变、发展，预见等。但作为逻辑语义学考察的对象，我们不需考虑它的具体含义，只是抽象地考察它作为某种对象。在可能世界语义学理论中，□α在某一可能世界w中的真值需要根据α在各个可能世界中的真值来确定。这就需要把□α与w联系起来，即可能世界之间需要有某种联系。因为，□α在w中的真值只与α在那些与w有某种关系的可能世界中的真值情况相关。而那些与w没有关系的可能世界中，无论α的真值情况如何都对□α的真值情况没有影响。比如，那些没有生物存在的可能世界不会影响“生物体必然要进行新陈代谢”这个命题在有生物存在的可能世界中的真值情况。所以，我们所要讨论的可能世界并不是任意的可能世界，而是与模态命题相关联的可能世界。这种可能世界之间的某种关系，可称为可及关系，一般用R表示。具体来说，如果可能世界w与可能世界w'有可通达关系，则称由w到w'有可及关系R，或者w可及w'记做wRw'或者Rww'。需注意的是，可及关系是有方向规定的。有时虽然可能世界w到可能世界w'有可及关系R，但从w'到w却不一定会有可及关系R。所以，可能世界语义学还要考虑可及关系的自返性、对称性、传递性等性质，这些性质对模态命题在可能世界中的真值情况有重要影响。

简单介绍了可能世界与可及关系这两个可能世界语义学的基本概念之后，便可以对模态命题的真值情况给予具体描述:

(3)□α在可能世界w中是真的，当且仅当，α在所有与w有可及关系的可能世界中都是真的。

(4)◇α在可能世界w中是真的，当且仅当，至少存在一个与w有可及关系的可能世界w'，使得α在w'中是真的。

由此可见，(3)、(4)与上面的(1)、(2)相比，加入了可及关系的概念，这就对模态命题的真值情况更加具体。由于模态命题的真值需要具体考虑命题所在的可能世界之间的可及关系，可能世界语义学也可称为关系语义学。

2.模态公式的语义分析

了解了可能世界语义学的基本思想，下面对一些模态命题形式做出解释，必须有三个要素:可能世界的集合W，可及关系R和赋值V。其中，W、R是解释的基础部分，它们形成的二元组，〈W，R〉称为框架。在框架〈W，R〉的基础上，增加赋值V，目的是使每一个公式在每个可能世界中都有唯一确定的真值。这样形成的三元组〈W，R，V〉，就是一个完整的解释，称为模型。具体定义如下:

定义1　(框架):设〈W，R〉是任意一个二元组，有序对〈W，R〉是一个框架，当且仅当，W是任一非空集合，R是W上的任意一个二元关系，即R≤W×W。

由于模态公式的真假是通过模型定义的，所以为了建立模型，需要引进赋值的概念:

定义2　(PM－赋值):设〈W，R〉是任意框架，V是〈W，R〉上对L_PM－公式的一个PM－赋值，当且仅当，V是由L_PM－公式集合与W的卡氏积到集合{0，1}上的映射，并且满足以下条件:对于任意的L_PM－公式α、β，任意w∈W;若α是命题变元，则V(α，w)=1或V(α，w)=0，二者只居其一。

PM－赋值V是一个函数，即V:Form(L_PM)×W→{0，1}。定义中只给出了V关于﹁和→这两个逻辑联结词的性质。根据V的定义和∧，∨，→，◇的语法定义可以得出V关于∧，∨，→，◇的性质。

定义3(模型):设〈W，R，V〉是任一有序三元组，〈W，R，V〉是一个L_PM－模型，当且仅当，〈W，R〉是一个框架，V是〈W，R〉上的一个PM－赋值。

理解了形式语义学的这三个基本概念，下面具体介绍模态形式的语义解释:

令V(α，w)=1表示命题α在可能世界w中是真的;V(α，w)=0表示命题α在可能世界w中是假的，则模态形式的解释为:

(1)□p

解释：V(□p，w)=1，当且仅当，对于任一w'，若Rww'，则V(p，w')=1

　　　V(□p，w)=0，当且仅当，存在一个w'，Rww'且V(p，w')=0

(2)◇p

解释：V(◇p，w)=1，当且仅当，存在一个w'，Rww'且V(p，w')=1

　　　V(◇p，w)=0，当且仅当，对于任一w'，若Rww'，则V(p，w')=0

(3)□□p

解释:V(□□p，w)=1，当且仅当，对任一w'，w″，若Rww'，Rw'w″，则V(p，w″)=1

(4)□◇p

解释:V(□◇p，w)=1，当且仅当，对任一w'，Rww'，存在w″，Rw'w″，且V(p，w″)=1

(5)◇□p

解释:V(◇□p，w)=1，当且仅当，存在w'，Rww'，对于所有w″，若，Rw'w″，则V(p，w″)=1

(6)◇◇p

解释:V(◇◇p，w)=1，当且仅当，存在w'，w″，使得Rww'与Rw'w″成立，并且V(p，w″)=1

3.模态系统的语义解释

前面我们用可能世界语义学讨论了模态公式的真假和有效性，下面简单介绍一下可能世界语义解释与模态逻辑系统的关系。

模态逻辑系统由公理和变形规则构成，是纯形式的系统。这些形式系统能否刻画模态命题之间的有效推理，必须通过对这些系统的语义解释来说明。所谓对模态系统的解释就是对系统的每一个可证公式(系统的公理或内定理)的解释。换句话说，如果一个解释是某一模态系统S的解释，则S的每一个可证公式在这一解释下都是有效的。如前所述，对于不同的解释，模态公式有着不同的有效性。与之相应，模态系统也就有了不同的解释。与模态公式四种不同的有效性相对应，模态系统S的解释也有四种，它们分别是S－模型、S－框架、S－框架类和S－模型类。

①S－模型:一个模型〈W，R，V〉是模态系统S的模型(S－模型)，记为M_S，当且仅当，对于任意L_PM－公式α，如果├_Sα，那么〈W，R，V〉╞α。

②S－框架:一个框架F是系统S－框架，记为F_S，当且仅当，对于F上的任意模型M，有M╞α。

③S－框架类:一个框架类F是S－框架类，记为F_S，当且仅当，对于任意F_S，有F_S∈F_S。

④S－模型类:一个模型类M是S－模型类，记为M_S，当且仅当，对于任意M_S，有M_S∈M_S。

在模态系统的这几种解释之间存在着一定的关系。例如，如果某一框架F是S－框架，则由F与任一赋值V所构成的模型〈F，S〉都是S－模型。所以，S－框架实际上可以看做由S－框架所构成的不同模型所组成的类。在对模态系统的四种不同解释中，M_S是最基本的解释，而M_S则是最一般的解释。

定义4　(可靠性)设S是任一系统，S是可靠的，当且仅当，对任意的S－公式α，如果α∈TH(S)，则α是S－有效的。

定理3　系统D、T、S4、S5、B和Tr都是可靠的。

定理4　设S是任一系统，S是可靠的，则S是语法一致的。

现代模态逻辑由于其内容较为抽象，只作为本科生的了解和参考内容，如有兴趣请参考周北海的《模态逻辑》一书，里面对模态逻辑的具体内容有较为详细的介绍。