目录 |
模态逻辑或者叫（不很常见）内涵逻辑，是处理用模态如“可能”、“或许”、“可以”、“一定”、“必然”等限定的句子的逻辑。模态逻辑可以用语义的“内涵性”来描述其特征：复杂公式的真值不能由子公式的真值来决定的。允许这种决定性的逻辑是“外延性的”，经典逻辑就是外延性的例子。模态算子不能使用外延语义来形式化：“乔治·布什是美国总统”和“2 + 2 = 4”是真的，但是“乔治·布什必然是美国总统”是假的，而“2 + 2 = 4是必然的”是真的。
在模态逻辑的最常见解释中，你要考虑“所有逻辑上可能的世界”。如果一个陈述在所有可能世界中是真的，则它是必然的真理。如果一个陈述碰巧在我们的世界中是真的，但不是在所有可能世界中是真的，则它是偶然的真理。在某些（不是必须在我们自己的）可能世界中是真的陈述叫做可能的真理。
这种"可能世界"是否是解释模态逻辑的最佳方式，怎样在文字上接受这种方言，是形而上学的鲜活的问题。例如，可能世界的方言可以把关于大脚怪的断言翻译为“有某个可能世界，在其中大脚怪存在”。要主张大脚怪的存在性是可能的，但不是现实的，你可以说“有某个可能世界，在其中大脚怪存在；但是在现实世界中，大脚怪不存在”。但是对使模态断言对我们负责的那个东西是什么仍是不清楚的。我们真的要宣称可能世界的存在性吗？它在每一点都同我们的现实世界一样真实，却惟独不是现实的。David Lewis强硬的说就是这样，可能世界同我们自己的世界一样真实。这种立场叫做“模态现实主义”。不足为奇的，多数哲学家不愿意接受这种特别的学说，在搜寻一种可替代的方式来释义我们的模态断言所蕴含的本体论承诺。
尽管亚里士多德的逻辑几乎全部都关注直言三段论的理论，他的著作还包含在模态逻辑要点上的一些延伸讨论（比如他著名的在解释篇§ 9中海战悖论），并且它们与潜在性和时间有关连。遵从他的著作，经院学者为模态逻辑的严格理论开发出了根基，大多在关于本质性和偶然性的陈述的逻辑的注释的上下文中。在中世纪的作家中，在William of Ockham和John Duns Scotus的著作中找到了关于模态逻辑的一些最重要的工作。
形式模态逻辑的缔造者是C. I. Lewis，他在专著《A Survey of Symbolic Logic》（1918）中介入了一个系统（后来叫做S3），并（同C. H. Langford一起）在书《Symbolic Logic》（1932）中介入了系统S1-S5。J. C. C. McKinsey在1941年使用代数方法（带有算子的布尔代数）来证明Lewis的S2和S4的可判定性。Saul Kripke从1959年开始为模态逻辑设计了关系语义或可能世界语义。Vaughan Pratt在1976年介入了动态逻辑。Amir Pnueli在1977年提出使用时态逻辑来公式化频繁操作并发程序的行为。
时间逻辑，在1957年由A. N. Prior发明，与模态逻辑有密切的关联，因为增加了模态算子[F]和[P]，分别意味着今后和至今，导致了时间逻辑的一个系统。时间逻辑的风味包括：命题动态逻辑（PDL），命题线性时间逻辑（PLTL），线性时间逻辑（LTL），计算树逻辑（CTL），Hennessy-Milner逻辑和T。
模态逻辑的数学结构，也就是扩充一元运算的布尔代数（经常叫做“模态代数”），开始出现于J. C. C. McKinsey在1941年对S2和S4是可判定性的证明，并于阿尔弗雷德·塔斯基和他的学生Bjarni Jonsson的工作（Jonsson与Tarski 1951-52）中得到完全能力。这项工作显示了S4和S5是内部代数的模型，它是最初设计用来捕获拓扑学的内部算子和闭包算子的性质的布尔代数的真扩展。