克里普克语义 · aiwiki.page

克里普克语义是语义学和模型论中的一类方法，在关系结构的各个点上求取逻辑公式的真值。这些点可以表示可能世界、信息状态或计算状态。点之间的关系决定了公式如何涉及其他点。其主要形式分别解释模态逻辑和直觉主义逻辑，并采用不同的规则来解释这两种逻辑的联结词。(ai.stanford.edu)

历史发展

索尔·A. 克里普克于1959年取得了具有重要影响的模态逻辑完备性成果，并在《模态逻辑的语义分析 I》（1963年）中系统论述了正规模态命题演算。他的《直觉主义逻辑的语义分析 I》（1965年）为直觉主义谓词逻辑引入了关系模型，并证明了这种解释下的完备性。这些进展使关系结构成为研究非经典逻辑的核心工具。(onlinelibrary.wiley.com)

框架、模型与模态真值

**克里普克框架**是一个有序对

F=(W,R),

其中， $W$ 是非空集合， $R\subseteq W\times W$ 是一个二元关系，称为可达关系。记号 $wRv$ 表示从 $w$ 可以到达 $v$ 。**克里普克模型**则在框架上增加一个赋值：

M=(W,R,V).

对于每个命题字母 $p$ ， $V(p)\subseteq W$ 指定了 $p$ 为真的那些点。(filosoficas.unam.mx)

满足关系的记号 $M,w\models\varphi$ 表示，在模型 $M$ 中， $\varphi$ 在点 $w$ 上为真。在经典模态逻辑中，命题逻辑的联结词保留其通常的局部含义：

\begin{aligned} M,w\models p &\iff w\in V(p),\\ M,w\models\neg\varphi &\iff M,w\not\models\varphi,\\ M,w\models\varphi\land\psi &\iff M,w\models\varphi\text{ 且 }M,w\models\psi. \end{aligned}

必然性和可能性则由涉及可达关系的条件定义：

\begin{aligned} M,w\models\Box\varphi &\iff \forall v\,(wRv\Rightarrow M,v\models\varphi),\\ M,w\models\Diamond\varphi &\iff \exists v\,(wRv\land M,v\models\varphi). \end{aligned}

因此， $\Box\varphi$ 涉及所有可达点，而 $\Diamond\varphi$ 涉及至少一个可达点。两者互为对偶： $\Diamond\varphi$ 等价于 $\neg\Box\neg\varphi$ 。(filosoficas.unam.mx)

例如，设从 $w$ 恰好可以到达 $u$ 和 $v$ ，且 $p$ 在 $u$ 上为真、在 $v$ 上为假。根据上述条件，有

M,w\models\Diamond p, \qquad M,w\not\models\Box p.

除非 $wRw$ ，否则 $p$ 在 $w$ 本身上的真值与这两个判断无关。在没有可达后继的点上，所有必然性公式都空真，所有可能性公式都为假。这些都是全称量化条件和存在量化条件的直接结果。

有效性与框架对应

逻辑有效性包含几个不同层次。一个公式如果在某个模型的每个点上都成立，就在该模型中有效；如果在某个框架的每个点上、在任意赋值下都成立，就在该框架上有效。在某类框架上有效，则要求它在该类中的每个框架上都有效。因此，仅检查一个赋值并不能证明公式在框架上有效。(ai.stanford.edu)

模态公理模式往往与可达关系的结构条件精确对应：

公理模式	公式	对应的框架条件
T	$\Box p\to p$	自反性： $wRw$
D	$\Box p\to\Diamond p$	序列性：每个点都有后继
4	$\Box p\to\Box\Box p$	传递性： $wRv\land vRu\Rightarrow wRu$
B	$p\to\Box\Diamond p$	对称性： $wRv\Rightarrow vRw$
5	$\Diamond p\to\Box\Diamond p$	右欧几里得性： $wRv\land wRu\Rightarrow vRu$

这些对应关系对所有赋值进行量化，而不只是针对某个特定模型的赋值。(ai.stanford.edu)

例如，自反性保证 T 成立，因为 $w$ 本身也在从它可达的点之中。反过来，如果 $wRw$ 不成立，就让 $p$ 在 $w$ 的所有后继上为真，而在 $w$ 上为假。此时， $\Box p$ 在 $w$ 上成立，但 $p$ 不成立，从而使 T 不成立。

可靠性与完备性

如果一个演绎系统的每个定理都在某类框架上有效，就称该系统相对于这类框架具有可靠性；如果在这类框架上有效的每个公式都是该系统的定理，就称它具有完备性。标准例子包括：T 相对于自反框架，S4 相对于自反且传递的框架，以及 S5 相对于可达关系为等价关系的框架。(filosoficas.unam.mx)

完备性并非自然成立。有些正规模态逻辑是克里普克不完备的：不存在一类普通克里普克框架，使得在这类框架上有效的公式恰好就是该逻辑的定理。这种不完备性涉及证明系统与普通框架语义之间的匹配问题，而不意味着无法在关系模型中求取公式的真值。(arxiv.org)

直觉主义强迫关系

直觉主义模型通常使用一个偏序集 $(W,\leq)$ ，将其解释为信息不断增长的各个阶段。原子命题的赋值具有持久性：

w\leq v,\quad w\Vdash p \quad\Rightarrow\quad v\Vdash p.

这里， $\Vdash$ 表示强迫关系。合取和析取在当前点上进行判断，而蕴涵则考察所有扩展：

w\Vdash\varphi\to\psi \iff \forall v\geq w\, (v\Vdash\varphi\Rightarrow v\Vdash\psi).

没有任何点强迫假命题 $\bot$ ，否定则定义为 $\neg\varphi=\varphi\to\bot$ 。因此，

w\Vdash\neg\varphi \iff \text{不存在强迫 }\varphi\text{ 的 }v\geq w.

持久性不仅适用于原子命题，也适用于所有公式。关键在于，不强迫一个命题与强迫该命题的否定并不相同。(princeton.edu)

要构造一个使排中律不成立的具体反模型，可以取两个点 $w<v$ ，并令 $p$ 仅在 $v$ 上被强迫。在 $w$ 上， $p$ 和 $\neg p$ 都不被强迫： $p$ 尚未得到确立，但扩展点 $v$ 确立了它。因此，

w\not\Vdash p\lor\neg p.

这个模型表示的是信息不完全，而不是矛盾。

对于直觉主义一阶逻辑，每个点还带有一个非空论域 $D(w)$ ，并且只要 $w\leq v$ ，就有 $D(w)\subseteq D(v)$ 。强迫存在量化公式要求在当前论域中有一个见证；强迫全称量化公式则需要考察每个后续点及其论域中的每个元素。(princeton.edu)

应用与局限

在计算机科学中，克里普克结构用来表示状态迁移系统。这些结构通常包含初始状态，以及一个记录各状态上哪些原子命题成立的标记函数。模型检测检验这些结构是否满足规约；时序逻辑还描述沿路径发生的行为，例如一个请求是否最终会得到响应。这为形式验证提供了支持，不过状态空间爆炸和系统模型不准确仍是重要的限制因素。(cs.cmu.edu)

可达关系不一定表示物理上的可能性。它可以编码计算中的状态迁移，也可以编码与主体所掌握信息相关的各种备选情形。因此，选择框架条件是选择数学模型的一部分，而不是对必然性或知识的所有解释作出普遍断言。(ai.stanford.edu)

双模拟揭示了表达能力的另一项局限：如果两个点的原子事实一致，且其迁移能够双向匹配，那么它们就满足相同的基本模态公式。代数语义、拓扑语义和邻域语义等其他框架，则提供了解释模态语言的不同方式。(ai.stanford.edu)

参考来源

Semantical Analysis of Modal Logic I Normal Modal Propositional Calculifilosoficas.unam.mx
Semantical Analysis of Intuitionistic Logic Iprinceton.edu
Modal Logic: A Semantic Perspectiveai.stanford.edu
A new version of an old modal incompleteness theoremarxiv.org
Introduction to Model Checkingcs.cmu.edu