模态逻辑

研究含有模态词“必然” “可能”的命题及其推理的逻辑学科。其历史可上溯到亚里士多德；其现代发展则始于美国逻辑学家刘易斯，他是现代模态逻辑的创始人。分为模态命题逻辑和模态谓词逻辑，分别由经典的命题逻辑和谓词逻辑作某种扩充所形成，主要的语义理论是可能世界语义学。

模态逻辑

指研究包含模态词“必然”、“可能”的模态命题及其推理的学科。早在二千多年前，亚里士多德在他的《工具论》一书中，就对模态命题作过大量的讨论，并提出了许多模态三段论的推理形式。本世纪初，美国逻辑学家刘易斯(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₁、S₂、S₃、S₄、S₅等五个模态逻辑公理系统，使模态逻辑进一步完善。其中，S₄是在T系统中加进一条新公理：
□p→□□p
而构成。从S₄系统中可以推出一些不属于T系统的公理。如果在T系统中加进下面的一条新公理：
◇p→□◇p
就构成了S₅系统。
模态逻辑的研究不限于模态命题系统。而且深入到模态命题的内部分析，建立了模态狭义谓词逻辑系统。此外，它在模态公式的判定问题和系统的完全性问题的研究上，都取得了成果。

模态逻辑

modal logic