关系语义发表评论(0)编辑词条

    Kripke 语义(也叫做关系语义或框架语义，并经常混淆于可能世界语义)是模态逻辑系统的形式语义，于 1950 年代晚期和 1960 年代早期由 Saul Kripke 建立。它后来为另一个非经典逻辑，最重要的直觉逻辑所接受。Kripke 语义的发现是非经典逻辑开发中重大突破，因为这种逻辑的模型论在 Kripke 之前实际上是不存在的。
模态逻辑的语义
对于我们的目的，模态逻辑的语言由命题变量，读者喜欢的布尔连结词的完备集合(比如 {→,¬} 或 {∨,∧,¬})，和模态算子 \Box (“必然性”)构成。对偶的模态算子 \Diamond (“可能性”) 定义为一个简写: \Diamond A:=\neg\Box\neg A。更多背景请参见模态逻辑。

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

Kripke 模型是 \Vdash> 三元组，这里的 是 Kripke 框架，而 \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 \VdashA 读做 “w 满足 A”，“A 满足于 w”，或 “w 力迫 A”。关系 \Vdash 叫做“满足关系”、“求值关系”或“力迫关系”。注意满足关系由它在命题变量上的值唯一确定。

关系语义-公式       
A 在下列之中是有效的:

模型 \Vdash>，如果对于所有 w ∈W 有 w \VdashA，
框架 ，如果对于 \Vdash 的所有可能的选择，它在 \Vdash> 中是有效的，
框架或模型的类 C，如果它在 C 的每个成员中都是有效的。
我们定义 Thm(C) 为在 C 中有效的所有公式的集合。反过来说，如果 X 是公式的集合，则设 Mod(X) 是使来自 X 的所有公式有效的所有框架的类。

一个模态逻辑(就是说一个公式的集合) L 关于框架的类 C 是可靠的，如果 L⊆Thm(C)。L 关于C 是完备的，如果 L⊇Thm(C)。
对应性和完备性
语义对于逻辑(就是推理系统)研究是有用的，条件是在语义蕴涵关系忠实的反映语法对应物 -- 推论关系 (可推导性)。所以知道哪个模态逻辑关于哪类 Kripke 框架是可靠的和完备的，并为它们确定这种类是关键性的。

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

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

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

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

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

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

L 的规范模型是 Kripke 模型 \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 的所有定理。通过 Zorn 引理，每个 L一致的集合都包含在一个 L-MCS 中，特别是在 L 中不可证明的所有公式都在规范模型中有一个反例。

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

我们说一个公式或公式的集合 X 关于 Kripke 的一个性质 P 是规范的，如果

X 在满足 P 的所有框架中是有效的，
对于包含 X 的任何正规模态逻辑 L，L 的规范模型底层框架满足 P。
明显的，公式的规范集合的并集自身是规范的。服从前面的讨论，由公式的规范集合公理化的任何逻辑是 Kripke 完备的和紧凑的。

公理 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 来证明逻辑的 Kripke 完备性: 所有正规模态逻辑关于模态代数的类都是完备的，而有限的模态代数可以变换成 Kripke 框架。作为例子，Robert Bull 使用这个方法证明了 S4.3 的所有普通扩展都有 FMP，并且是 Kripke 完备的。

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

w\Vdash\Box_i A 当且仅当 \forall u\,(w\;R_i\;u\Rightarrow u\Vdash A)。
由 Tim Carlson 发现的简化的语义，经常用于多模态可证明性逻辑。Carlson 模型是结构 ，带有一个单一的可及关系 R，和给每个模态的子集 Di ⊆ W。满足性定义为

w\Vdash\Box_i A 当且仅当 \forall u\in D_i\,(w\;R\;u\Rightarrow u\Vdash A)。
Carlson 模型比通常的多模态 Kripke 模型易于形象化和使用；但是，Kripke 完备的多模态逻辑是 Carlson 不完备的。

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

直觉 Kripke 模型是一个三元组 \Vdash>，这里的 是传递的和自反的 Kripke 框架(就是说可及关系是预序)，而 \Vdash 满足下列条件:

如果 p 是命题变量，w ≤ u，而且 w \Vdashp，则 u \Vdashp (坚持条件)，
w \VdashA ∧ B 当且仅当 w \VdashA 并且 w \VdashB，
w \VdashA ∨ B 当且仅当 w \VdashA 或者 w \VdashB，
w \VdashA → B 当且仅当对于所有 u ≥ w，u \VdashA 蕴含 u \VdashB，
无 w \Vdash⊥。
直觉逻辑关于它的 Kripke 语义是可靠的和完备的，并且它有 FMP。

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

Mu 的域包含在 Mv 的域中，
Mu 和 Mv 中的函数符号实现一致于 Mu 的元素，
对于每个 n 元谓词 P 和元素 a1,...,an ∈Mu: 如果 P(a1,...,an) 成立于 Mu，则它成立于 Mv。
给出经由 Mw 的元素的变量求值 e，我们定义满足关系 w \VdashA【e】:

w \VdashP(t1,...,tn)【e】 当且仅当 'P(t1【e】,...,tn【e】) 成立于 Mw，
w \Vdash(A ∧ B)【e】 当且仅当 w \VdashA【e】 并且 w \VdashB【e】，
w \Vdash(A ∨ B)【e】 当且仅当 w \VdashA【e】 或者 w \VdashB【e】，
w \Vdash(A → B)【e】 当且仅当对于所有的 u ≥ w，u \VdashA【e】 蕴含 u \VdashB【e】，
无 w \Vdash⊥【e】，
w \Vdash(∃x A)【e】 当且仅当存在一个 a ∈Mw，使得 w \VdashA【e(x→a)】，
w \Vdash(∀x A)【e】 当且仅当对于所有的 u ≥ w 和所有的 a ∈Mu，u \VdashA【e(x→a)】。
这里的 e(x→a) 是给予 x 值 a 的求值，在其他方面一致于 e。

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

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

f 保留可及关系，就是说 u R v 蕴涵 f(u) R’ f(v)，
在 f(u) R’ v’ 的时候，有一个 v ∈ W 使得 f(v)=v’。
Kripke 模型 \Vdash> 和 \Vdash’> 的 p-态射是它们的底层框架的 p-态射 f:W → W’，它满足

对于任何命题变量 p，w \Vdashp 当且仅当 f(w) \Vdash’p。
P-态射是特殊种类的双仿(bisimulation)。一般的说，在框架 和 之间的 双仿是关系 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 \Vdashp 当且仅当 w’ \Vdash’p。
从这个定义我们得到的关键性质是模型的双仿(所以也是 p-态射)保持所有公式的满足性，而不只是命题变量。

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

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

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

f 是满射，
f 保持可及关系，和(在两个方向上)变量 p ∈ X 的满足性，
如果 f(u) R’ f(v) 并且 u \Vdash \BoxA，这里的 \BoxA ∈X，则 v \VdashA。
得到了 f 保持来自 X 的所有公式的满足性。在典型的应用中，我们把 f 采纳为在W 在下列关系上对份额的投影

u ≡X v 当且仅当对于所有 A ∈X，u \VdashA 当且仅当 v \VdashA。
同在拆分的情况下一样，定义可及关系在份额变化上。

历史和术语
Kripke 语义不是 Kripke 首创的，以上述方式给出的基于使求值相对于节点的语义早于 Kripke 的工作许久:

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

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