模态逻辑

模态逻辑是逻辑学的一个分支，研究涉及模态的推理，即带有“必然”“可能”等限定的推理。狭义的模态逻辑研究必然性和可能性；广义上，它还包括表示知识、信念、义务、时间和行动的系统。“模态逻辑”并不指某一种演算，而是指一族形式系统，其中的算子具有不同的解释，并遵循不同的原则。这些系统在哲学、数学和计算领域都有应用。(plato.stanford.edu)

历史发展

亚里士多德在其三段论理论中考察了涉及必然性和可能性的推理。现代模态逻辑则从对蕴涵的公理化研究中发展而来。克拉伦斯·欧文·刘易斯在《符号逻辑概论》（1918年）中引入了严格蕴涵系统；他与库珀·哈罗德·兰福德合著的《符号逻辑》（1932年）则提出了 S1–S5 系统。严格蕴涵表达的是前提为真而结论为假这一情况不可能发生，而不只是一个实质蕴涵命题为真。(iep.utm.edu)

在20世纪50年代至60年代初，索尔·克里普克、斯蒂格·坎格尔、雅各·欣蒂卡等人提出的关系语义学方法，为众多模态系统提供了解释。这些方法的核心创新在于：相对于可及的备选情形来判定必然性，而不是不加区分地考察所有可能世界。这使公理化演算与数学上明确定义的模型联系起来。(hume.ucdavis.edu)

语言与解释

基本的命题模态逻辑在命题逻辑的基础上增加了两个算子：

(\Box\varphi)：“必然有 (\varphi)。”
(\Diamond\varphi)：“可能有 (\varphi)。”

其句法允许使用原子命题、普通命题联结词，以及反复嵌套的模态算子。因此，(\Box\Diamond p) 表示必然的可能性，而 (\Diamond\Box p) 表示可能的必然性。在标准的经典模态系统中，这两个算子互为对偶：

[ \Diamond\varphi \equiv \neg\Box\neg\varphi. ]

因此，一个命题是可能的，意味着它的否定并非必然。模态算子不是普通的真值函数联结词：仅仅知道 (p) 实际上是否为真，并不足以确定它是否必然或可能。(cs.stanford.edu)

算子的作用域十分重要。公式 (\Box(p\rightarrow q)) 表示该条件命题是必然的，而 (p\rightarrow\Box q) 表示如果 (p) 为真，那么 (q) 是必然的。这两种表述通常不能互换。严格蕴涵通常用前一种公式表示。(cs.stanford.edu)

可能世界语义

克里普克语义在各个可能世界中，或更一般地说，在各个状态中判定公式的真值。一个模型由非空集合 (W)、定义在 (W) 上的可及二元关系 (R)，以及为各个世界中的原子命题赋予真值的赋值函数组成。不含赋值函数的二元组 ((W,R)) 称为框架。(cs.stanford.edu)

模态公式的真值条件如下：

[ M,w\models\Box\varphi \quad\text{当且仅当}\quad M,v\models\varphi \text{ 对每个满足 }wRv\text{ 的 }v\text{ 都成立}; ]

[ M,w\models\Diamond\varphi \quad\text{当且仅当}\quad M,v\models\varphi \text{ 对某个满足 }wRv\text{ 的 }v\text{ 成立}. ]

可及关系规定了从某一给定状态出发，哪些备选情形需要纳入考察。根据不同的解释，这些情形可以是形而上学意义上的可能情形、信息上容许的备选情形，或通过某个行动能够到达的状态。这套形式工具本身并不能决定可能世界的形而上学地位。(cs.stanford.edu)

公式在一个框架上的逻辑有效性，要求它在每一种赋值下、每一个世界中都为真。公式在一类框架上有效，则要求它在该类的每个框架上都有效。这样便区分了某个特定模型中的真与支配整个模态系统的原则。(iep.utm.edu)

主要系统

基本的正规模态逻辑 K 包含命题重言式、分配公理模式

[ \Box(\varphi\rightarrow\psi) \rightarrow(\Box\varphi\rightarrow\Box\psi), ]

并以肯定前件式和必然化规则作为推理规则。必然化规则允许在 (\varphi) 是定理时推出 (\Box\varphi)，但不能仅凭一个尚未解除的假设作此推断。K 不对可及关系施加任何特殊条件。更强的系统则添加与框架限制相对应的原则。(plato.stanford.edu)

系统	在 K 的基础上添加的原则	对应框架的特征
T	(\Box p\rightarrow p)	自反
S4	T 以及 (\Box p\rightarrow\Box\Box p)	自反且传递
S5	T 以及 (\Diamond p\rightarrow\Box\Diamond p)	可及关系是[[equivalence-relation

这些系统是不同的形式化方案，而不是对某种普遍正确的逻辑逐步逼近的结果。它们是否合适，取决于所要表达的模态。例如，义务不一定描述实际发生的事情，因此，类似 T 的原则不适用于通常意义上的义务。(plato.stanford.edu)

量化与哲学问题

量化模态逻辑将模态算子与一阶逻辑结合起来。它区分作用于整个命题的从言模态（de dicto）与涉及某个对象的从物模态（de re）。例如，(\Box\exists x,F(x)) 表示必然存在具有性质 (F) 的事物；(\exists x,\Box F(x)) 则表示存在某个必然具有性质 (F) 的对象。前一个公式并不一定要求有同一个对象在所有相关的备选情形中都满足该条件。(cs.stanford.edu)

解释必须明确：各个世界的论域是保持不变还是可以变化，以及如何在不同的备选情形中解释对象和指称表达式。这些选择会影响量化与模态之间的相互作用，并使模态逻辑与形而上学中关于存在和同一性的问题联系起来。(hume.ucdavis.edu)

历史发展

语言与解释

可能世界语义

主要系统

量化与哲学问题

相关逻辑与应用