关系语义

克里普克语义(也叫做关系语义或框架语义，并经常混淆于可能世界语义)是模态逻辑系统的形式语义，于 1950 年代晚期和 1960 年代早期由索尔·阿伦·克里普克建立。它后来为另一个非经典逻辑，最重要的直觉逻辑所接受。克里普克语义的发现是非经典逻辑开发中重大突破，因为这种逻辑的模型论在克里普克之前实际上是不存在的。

模态逻辑的语义

对于我们的目的，模态逻辑的语言由命题变量，读者喜欢的布尔连结词的完备集合(比如 {→,¬} 或 {∨,∧,¬})，和模态算子 $\Box$ (“必然性”)构成。对偶的模态算子 $\Diamond$ (“可能性”) 定义为一个简写: $\Diamond A:=\neg \Box \neg A$ 。更多背景请参见模态逻辑。

基本定义

克里普克框架或模态框架是 <W,R> 对，这里的 W 是非空集合，R 是在 W 上的二元关系。W 的元素叫做节点或世界，而 R 叫做可及关系。

克里普克模型是 $<W,R,\Vdash >$ 三元组，这里的 $<W,R>$ 是克里普克框架，而 $\Vdash$ 是在 W 的节点和模态公式之间的如下关系:

$w\Vdash \neg A$ 当且仅当 $w\not \Vdash A$ ，
$w\Vdash A\to B$ 当且仅当 $w\not \Vdash A$ 或 $w\Vdash B$ ，
$w\Vdash \Box A$ 当且仅当 $\forall u\,(w\;R\;u\Rightarrow u\Vdash A)$ 。

我们把 $w\Vdash A$ 读做 “w 满足 A”，“A 满足于 w”，或 “w 力迫 A”。关系 $\Vdash$ 叫做“满足关系”、“求值关系”或“力迫关系”。注意满足关系由它在命题变量上的值唯一确定。

公式 A 在下列之中是有效的:

模型 <W,R, $\Vdash$ >，如果对于所有 w ∈W 有 w $\Vdash$ A，
框架 <W,R>，如果对于 $\Vdash$ 的所有可能的选择，它在 <W,R, $\Vdash$ > 中是有效的，
框架或模型的类 C，如果它在 C 的每个成员中都是有效的。

我们定义 Thm(C) 为在 C 中有效的所有公式的集合。反过来说，如果 X 是公式的集合，则设 Mod(X) 是使来自 X 的所有公式有效的所有框架的类。

一个模态逻辑(就是说一个公式的集合) L 关于框架的类 C 是可靠的，如果 L⊆Thm(C)。L 关于C 是完备的，如果 L⊇Thm(C)。

对应性和完备性

语义对于逻辑(就是推理系统)研究是有用的，条件是在语义蕴涵关系忠实的反映语法对应物 -- 推论关系 (可推导性)。所以知道哪个模态逻辑关于哪类克里普克框架是可靠的和完备的，并为它们确定这种类是关键性的。

对于克里普克框架的任何类 C，Thm(C) 是正规模态逻辑；特别是，最小化正规模态逻辑 K 的定理，在所有克里普克模型中都是有效的。不幸的是，逆命题不是一般性成立的: 有克里普克不完备的正规模态逻辑。事实上这不是问题，因为实际中研究的多数模态系统关于由简单条件所描述的框架类是完备的。

正规模态逻辑 L 对应于框架类 C，条件是 C=Mod(L)。换句话说，C 是 L 关于 C 是可靠的最大的框架类；随后 L 是克里普克完备的当且仅当它关于它所对应的类是完备的。

作为一个例子，考虑模式 T : $\Box$ A → A。T 在任何自反的框架 <W,R> 中是有效的: 如果 w $\Vdash \Box$ A，则 w $\Vdash$ A，因为 w R w。在另一方面，使 T 有效的框架必须是自反的: 固定 w ∈W，并定义命题变量 p 的满足为如下: u $\Vdash$ p 当且仅当 w R u。那么 w $\Vdash \Box$ p，所以 w $\Vdash$ p 于 T，这意味着 w R w 使用了 $\Vdash$ 的定义。我们见到 T 对应于自反的克里普克框架的类。

特征化 L 的对应类经常比证明它的完备性要容易许多，所以对应性充当完备性证明的指导。对应性还用于证实模态逻辑的不完备性: 假定 L₁⊆L₂ 是对应于同一个框架类的正规模态逻辑，L₁ 不证明 L₂ 的所有定理。那么 L₁ 是克里普克不完备的。例如，模式 $\Box (A\equiv \Box A)\to \Box A$ 生成一个不完备的逻辑，因为它对应于同 GL 一样的框架类(viz. 传递性和逆良基的框架)，但是它不证明 $\Box A\to \Box \Box A$ 。

在下表中给出常见模态公理和它们对应的类的列表。注意: 公理的名字经常是多变的。

**常见模态公理模式**
名字	公理	框架条件
T	$\Box A\to A$	自反的
4	$\Box A\to \Box \Box A$	传递的
D	$\Box A\to \Diamond A$	连续的: $\forall w\,\exists v\,(w\;R\;v)$
B	$A\to \Box \Diamond A$	对称的
5	$\Diamond A\to \Box \Diamond A$	欧几里德式的: $w\;R\;u\land w\;R\;v\Rightarrow u\;R\;v$
GL	$\Box (\Box A\to A)\to \Box A$	R 传递的, R^-1 良基的
Grz	$\Box (\Box (A\to \Box A)\to A)\to A$	R 自反的和传递的, R^-1−Id 良基的
H	$\Box (\Box A\to B)\lor \Box (\Box B\to A)$	$w\;R\;u\land w\;R\;v\Rightarrow u\;R\;v\lor v\;R\;u$
M	$\Box \Diamond A\to \Diamond \Box A$	(一个复杂的二阶性质)
G	$\Diamond \Box A\to \Box \Diamond A$	$w\;R\;u\land w\;R\;v\Rightarrow \exists x\,(u\;R\;x\land v\;R\;x)$

下面是一些常见正规模态逻辑系统的列表。对于其中一些的框架条件是简化了的: 逻辑关于在表中给出的框架类是完备的，但是它们可能对应于更大的一类框架。

**常见正规模态逻辑**
名字	公理	框架条件
K	-	所有框架
T	T	自反的
K4	4	传递的
S4	T, 4	预序
S5	T, 5 或 D, B, 4	等价
S4.3	T, 4, H	全序
S4.1	T, 4, M	预序, $\forall w\,\exists u\,(w\;R\;u\land \forall v\,(u\;R\;v\Rightarrow u=v))$
S4.2	T, 4, G	有向预序
GL	GL 或 4, GL	有限的严格偏序
Grz, S4Grz	Grz 或 T, 4, Grz	有限的偏序
D	D	连续的
D45	D, 4, 5	传递的、连续的和欧几里德式的

典范模型

对于任何正规模态逻辑 L，我们可以构造一个克里普克模型(称为典范模型)，它且只有它使 L 的定理有效，通过接纳使用极大一致集合作为模型的标准技术。典范克里普克模型扮演的角色类似于在代数语义中的 Lindenbaum–Tarski代数构造。

公式集合 L是一致的，如果从它们、L 的公理和肯定前件中不能推导出矛盾。极大 L一致的集合(简写为 L-MCS)是没有真L一致的超集的 L一致的集合。

L 的典范模型是克里普克模型 <W,R, $\Vdash$ >，这里的 W 是所有L-MCS，而关系 R 和 $\Vdash$ 为如下:

X\;R\;Y

当且仅当对所有的公式

A

，如果

\Box A\in X

则

A\in Y

，

X\Vdash A

当且仅当

A\in X

。

典范模型是 L 的模型，因为所有的 L-MCS 包含 L 的所有定理。通过佐恩引理，每个 L一致的集合都包含在一个 L-MCS 中，特别是在 L 中不可证明的所有公式都在典范模型中有一个反例。

典范模型的主要应用是完备性证明。例如，K 的典范模型的性质直接蕴含 K 关于所有克里普克框架类的完备性。这个论证不适合任意的 L，因为没有对典范模型的底层框架满足 L 的框架条件的担保。

我们说一个公式或公式的集合 X 关于克里普克的一个性质 P 是典范的，如果

X 在满足 P 的所有框架中是有效的，
对于包含 X 的任何正规模态逻辑 L，L 的典范模型底层框架满足 P。

明显的，公式的典范集合的并集自身是典范的。服从前面的讨论，由公式的典范集合公理化的任何逻辑是克里普克完备的和紧致的。

公理 T、4、D、B、5、H、G(和它们的任意组合)都是典范的。GL 和 Grz 不是典范的，因为他们不是紧凑的。公理 M 自身不是规范的(Goldblatt, 1991)，但是组合的逻辑 S4.1(事实上甚至 K4.1) 是典范的。

一般的，给定的公理是否是典范的是不可判定的。不过我们知道一个好的充分条件: H。Sahlqvist 识别了如下广泛的一类公式(现在叫做Sahlqvist公式)

Sahlqvist 公式是典范的，
对应于 Sahlqvist 公式的框架类是一阶可定义的，
有计算对一个给定的 Sahlqvist 公式的对应框架条件的算法。

这是一个非常强力的准则；例如，上面列出的典范的所有公理是实际上的(等价于) Sahlqvist 公式。

有限模型性质

逻辑拥有有限模型性质(FMP)，如果它关于有限框架的类是完备的。这个概念的主要应用之一是可判定性问题: 它服从 Post定理，有 FMP 的递归公理化的模态逻辑 L 是可判定的，倘若给定的有限框架是否是 L 的模型是可判定的。特别是，有 FMP 的所有的有限可公理化的逻辑都是可判定的。

有各种方法为给定的逻辑建立 FMP。精练并扩展规范模型构造通常就行了，使用工具如过滤或拆分。还有一种可能性，给予免切的相继式演算的完备性证明通常直接产生有限模型。

多数实际上使用的模态系统(包括所有上面列出的)都有 FMP。

在某些情况下，我们可以使用 FMP 来证明逻辑的克里普克完备性: 所有正规模态逻辑关于模态代数的类都是完备的，而有限的模态代数可以变换成克里普克框架。作为例子，Robert Bull 使用这个方法证明了 S4.3 的所有普通扩展都有 FMP，并且是克里普克完备的。

多模态逻辑

克里普克语义对有多于一个模态的逻辑有直接的推广。带有 $\{\Box _{i};\,i\in I\}$ 作为必然性算子的集合的语言的克里普克框架，由对每个 i ∈I 装备上二元关系 R_i 一个非空集合 W构成。满足关系的定义修改为如下:

w\Vdash \Box _{i}A

当且仅当

\forall u\,(w\;R_{i}\;u\Rightarrow u\Vdash A)

。

由 Tim Carlson 发现的简化的语义，经常用于多模态可证明性逻辑。Carlson 模型是结构 <W,R,{D_i}_i∈I,⊩>，带有一个单一的可及关系 R，和给每个模态的子集 D_i ⊆ W。满足性定义为

w\Vdash \Box _{i}A

当且仅当

\forall u\in D_{i}\,(w\;R\;u\Rightarrow u\Vdash A)

。

Carlson 模型比通常的多模态克里普克模型易于形象化和使用；但是，克里普克完备的多模态逻辑是 Carlson 不完备的。

直觉逻辑的语义

直觉逻辑的克里普克语义服从和模态逻辑的语义同样的原理，但是它使用了满足的不同的定义。

直觉克里普克模型是一个三元组 $<W,\leq ,\Vdash >$ ，这里的 $<W,\leq >$ 是偏序(也有说是预序) 克里普克框架，而 $\Vdash$ 满足下列条件:

如果 $p$ 是命题变量， $w\leq u$ ，而且 $w\Vdash p$ ，则 $u\Vdash p$ (单调性要求)，
$w\Vdash A\land B$ 当且仅当 $w\Vdash A$ 并且 $w\Vdash B$ ，
$w\Vdash A\lor B$ 当且仅当 $w\Vdash A$ 或者 $w\Vdash B$ ，
$w\Vdash A\rightarrow B$ 当且仅当对于所有 $u\geq w$ ， $u\Vdash A$ 蕴含 $u\Vdash B$ ，
$w\Vdash \lnot A$ 当且仅当没有 $u\geq w$ ， $w\Vdash A$ ，

直觉逻辑关于它的克里普克语义是可靠的和完备的，并且它有 FMP。

直觉一阶逻辑

设 L 是一阶语言。L 的克里普克模型是三元组 <W,≤,{M_w}_w∈W>，这里的 <W,≤> 是直觉克里普克框架，M_w 是 w ∈W 每个节点的(经典) L-结构，而下列相容性条件只要在 u ≤ v 时都是成立的:

M_u 的域包含在 M_v 的域中，
M_u 和 M_v 中的函数符号实现一致于 M_u 的元素，
对于每个 n 元谓词 P 和元素 a₁,...,a_n ∈M_u: 如果 P(a₁,...,a_n) 成立于 M_u，则它成立于 M_v。

给出经由 M_w 的元素的变量求值 e，我们定义满足关系 w $\Vdash$ A[e]:

w $\Vdash$ P(t₁,...,t_n)[e] 当且仅当 P(t₁[e],...,t_n[e]) 成立于 M_w，
w $\Vdash$ (A ∧ B)[e] 当且仅当 w $\Vdash$ A[e] 并且 w $\Vdash$ B[e]，
w $\Vdash$ (A ∨ B)[e] 当且仅当 w $\Vdash$ A[e] 或者 w $\Vdash$ B[e]，
w $\Vdash$ (A → B)[e] 当且仅当对于所有的 u ≥ w，u $\Vdash$ A[e] 蕴含 u $\Vdash$ B[e]，
w $\Vdash$ ¬ A[e] 当且仅当没有 u ≥ w，u $\Vdash$ A[e]，
w $\Vdash$ (∃x A)[e] 当且仅当存在一个 a ∈M_w，使得 w $\Vdash$ A[e(x→a)]，
w $\Vdash$ (∀x A)[e] 当且仅当对于所有的 u ≥ w 和所有的 a ∈M_u，u $\Vdash$ A[e(x→a)]。

这里的 e(x→a) 是给予 x 值 a 的求值，在其他方面一致于 e。

Kripke-Joyal 语义

作为独立开发的层论的一部分，在 1965 年左右认识到克里普克语义密切相关于在 topos论中对存在量化的处理。就是对一个层的截面的存在性的'局部'示象是一种'可能性'的逻辑。因为这种开发是很多人的工作，比之于理论更合于概念上洞察的天性，归与荣誉不是很容易的。Kripke-Joyal 语义这个名称经常用做这种联系。

模型构造

同在经典的模型论中一样，有从其他模型构造一个新的克里普克模型的方法。

在克里普克语义中天然的同态叫做p-态射(它是伪满射的简写，但这个术语很少用)。克里普克框架 <W,R> 和 <W’,R’> 的 p-态射是一个映射 f:W → W’ 满足

f 保留可及关系，就是说 u R v 蕴涵 f(u) R’ f(v)，
在 f(u) R’ v’ 的时候，有一个 v ∈ W 使得 f(v)=v’。

克里普克模型 <W,R, $\Vdash$ > 和 <W’,R’, $\Vdash$ ’> 的 p-态射是它们的底层框架的 p-态射 f:W → W’，它满足

对于任何命题变量 p，w

\Vdash

p 当且仅当 f(w)

\Vdash

’p。

P-态射是特殊种类的双仿(bisimulation)。一般的说，在框架 <W,R> 和 <W’,R’> 之间的双仿是关系 B ⊆ W × W’，它满足下列 “zig-zag” 性质:

如果 u B u’ 并且 u R v，则存在 v’ ∈ W’ 使得 v B v’，
如果 u B u’ 并且 u’ R’ v’，则存在 v ∈ W 使得 v B v’。

模型的双仿是对保持原子公式的力迫的补充要求:

对于任何命题变量 p，如果 w B w’，则 w

\Vdash

p 当且仅当 w’

\Vdash

’p。

从这个定义我们得到的关键性质是模型的双仿(所以也是 p-态射)保持所有公式的满足性，而不只是命题变量。

我可以使用拆分(unravelling)把克里普克模型变换成树。给出一个模型 <W,R, $\Vdash$ > 和固定的节点 w₀ ∈ W，我们定义一个模型 <W’,R’, $\Vdash$ ’>，这里的 W’ 是所有有限序列 s=<w₀,w₁,...,w_n> 的集合，使得对于所有 i<n 和 s $\Vdash$ p，w_i R w_i+1 当且仅当对于所有变量 p，w_n $\Vdash$ p。定义可及关系 R’ 变化；在最简单的情况下我们置

<w₀,w₁,...,w_n> R’ <w₀,w₁,...,w_n,w_n+1>,

但是很多应用需要这个关系的自反与/或传递闭包，或类似的变更。

过滤是 p-态射的一个变种。设 X 是在采纳子公式(subformulas)下闭合的公式的集合。模型 <W,R, $\Vdash$ > 的 X-过滤是从W 到模型 <W’,R’, $\Vdash$ ’> 的映射 f，使得

f 是满射，
f 保持可及关系，和(在两个方向上)变量 p ∈ X 的满足性，
如果 f(u) R’ f(v) 并且 u $\Vdash \Box$ A，这里的 $\Box$ A ∈X，则 v $\Vdash$ A。

得到了 f 保持来自 X 的所有公式的满足性。在典型的应用中，我们把 f 采纳为在W 在下列关系上对份额的投影

u ≡_X v 当且仅当对于所有 A ∈X，u

\Vdash

A 当且仅当 v

\Vdash

A。

同在拆分的情况下一样，定义可及关系在份额变化上。

一般框架语义

克里普克语义的主要缺陷是存在克里普克不完备逻辑和完备但不紧致的逻辑。可以使用来代数语义的想法，通过对克里普克装备限制可能求值的集合的额外结构来修正。这引发了一般框架语义。

历史和术语

克里普克语义不是克里普克首创的，以上述方式给出的基于使求值相对于节点的语义早于克里普克的工作许久:

Carnap 好像是首先有了这种想法，通过给予求值函数以莱布尼兹的可能世界为范围的一个参数的方式，对必然性和可能性的模态给出一种可能世界语义。Bayart 进一步发展了这种想法，但是他们都没能给出 Tarski 介入的这种风格的满足的递归定义；
Jónsson 和 Tarski 给出了仍然影响着当代模态逻辑研究的表达语义的方式，就是代数方法，这包含了克里普克语义的很多关键想法。他们把这个想法应用于直觉逻辑的语义研究，但没有见到与模态逻辑的联系；
Kanger 对模态逻辑的释义给出了更加复杂的方式，但是包含了克里普克方式的很多关键想法。他首先注意到在关于可及关系的条件和 Lewis-风格的模态逻辑公理之间的联系。但是 Kanger 没能给出对他的系统的完备性证明；
Jaakko Hintikka 在他的论文中介入了是克里普克语义的简单变体的认识逻辑，等同于通过最大化一致集合的方式构造求值的塑造。他没能为认识逻辑给出推理规则，所以没能给出完备性证明；
Richard Montague 有了包含在克里普克工作中的很多关键想法，但是他没有把它们当作是重要的，所以一直没有发表直到克里普克的论文出版在逻辑学社区中造成了轰动之后；
Evert W. Beth 为直觉逻辑提出了一种基于树的语义，它极其类似于克里普克语义，除了使用了更加麻烦的满足定义之外。

尽管克里普克语义的根本思想在克里普克首次发表之前就广为流传了，克里普克关于模态逻辑的工作仍可恰当的当作是开拓性的。最重要的是，克里普克是第一个为模态逻辑证明了完备性定理的人，并且克里普克识别了最弱的正规模态逻辑。

尽管克里普克的工作有开创性贡献，很多模态逻辑学家反对术语 克里普克语义，因为这是对先驱们做的重要贡献的失礼。反对另一个最广泛使用的术语可能世界语义的理由是它不适合应用于不是可能性和必然性的模态，比如在认识或道义逻辑中。他们喜欢术语关系语义或框架语义。

引用

Modal Logic. P. Blackburn, M. de Rijke, Y. Venema. Cambridge University Press, 2001.
Basic Modal Logic. R. A. Bull and K. Segerberg. In The Handbook of Philosophical Logic, volume 2, pages 1--88. Kluwer, 1984.
A New Introduction to Modal Logic. G. E. Hughes, M. J. Cresswell. Routledge, 1996.
Modal Logic. A. Chagrov, M. Zakharyaschev. Oxford University Press, 1997.
Modal Logic （页面存档备份，存于互联网档案馆）. J. Garson. In E. N. Zalta, editor, The Stanford Encyclopaedia of Philosophy
Mathematical Modal Logic: a View of its Evolution （页面存档备份，存于互联网档案馆）. Robert Goldblatt （页面存档备份，存于互联网档案馆）. In Journal of Applied Logic, vol. 1(5-6):309-392, 2003.
Intuitionistic Logic. D. van Dalen. In The Handbook of Philosophical Logic, volume 3, pages 225--339. Reidel, 1986.
Elements of Intuitionism. M. Dummett. Clarendon Press, 1977.
Intuitionistic Logic, Model Theory and Forcing. M. Fitting. North-Holland, 1969.
Sheaves in Geometry and Logic. S. Mac Lane and I. Moerdijk. Springer-Verlag, 1991.

参见

外部链接

Introduction to Mathematical Logic （页面存档备份，存于互联网档案馆） by Drs. Detlovs and Podnieks. Chapter 4, Section 4: "Constructive Propositional Logic — Kripke Semantics".
Kripke Models, a Word document by John P. Burgess.