模态逻辑

指研究包含模态词“必然”、“可能”的模态命题及其推理的学科。早在二千多年前，亚里士多德在他的《工具论》一书中，就对模态命题作过大量的讨论，并提出了许多模态三段论的推理形式。本世纪初，美国逻辑学家刘易斯(C?I?Lewis)用数理逻辑的方法和观点对模态逻辑作了系统的研究，奠定了现代模态逻辑的基础。

模态逻辑把命题分为三种基本类型：必然命题、实然命题和可能命题。例如，“金属受热必然膨胀”，“3大于2”，“火星上可能有生物”分别属于这三种类型命题。模态逻辑把“必然”，“可能”作为模态算子，用符号“□”和“◇”分别代表它们。这样，□p、◇p等就是模态命题，p、q等就是实然命题。

模态逻辑分析了这三种类型的命题，建立了下面一些普遍成立的关系式：

□p→p (如果必然p，则p)

p→◇?p (如果p，则可能p)

◇p?◇p (必然p，当且仅当非p不可能)◇p?□?p (可能p，当且仅当不必然非p)并用模态算子定义了严格蕴涵，以同古典逻辑中的实质蕴涵相区别，因为实质蕴涵只考虑蕴涵式的前件和后件的真假关系，而不涉及它们意义上的必然联系，容易产生“蕴涵怪论”。模态逻辑用符合“ ”表示严格蕴涵，把它定义为

p q=?◇(p ∧?q)

即“p严格蕴涵q，等值于不可能p真而q假”。这样定义后的蕴涵式，反映了前件与后件之间的必然联系。

为了把模态逻辑中的真命题作为一个整体来对待，逻辑学家构造了若干个模态逻辑公理系统，其中一个最弱的系统是由罗伯特?菲斯(Robetr Feys)提出的T系统。T系统除了把命题演算的重言式都作为自己的公理外，增加了下面两条公理：

□(p→q) □p→◇p

□(p →q)→(□p→□q)

除了代入规则和分离规则外，又增加一条必然规则作为变形规则，由此推演出其余的真的模态命题。

T系统不能处理由重叠模态词所构成的模态命题，如□□p，◇□p等等。为了解决这个问题，刘易斯构造了S

1

、S

2

、S

3

、S

4

、S

5

等五个模态逻辑公理系统，使模态逻辑进一步完善。其中，S

4

是在T系统中加进一条新公理：

□p→□□p

而构成。从S

4

系统中可以推出一些不属于T系统的公理。如果在T系统中加进下面的一条新公理：

◇p→□◇p

就构成了S

5

系统。

模态逻辑的研究不限于模态命题系统。而且深入到模态命题的内部分析，建立了模态狭义谓词逻辑系统。此外，它在模态公式的判定问题和系统的完全性问题的研究上，都取得了成果。