关系语义

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

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

Kripke 模型是 三元组，这里的 是 Kripke 框架，而 是在 W 的节点和模态公式之间的如下关系:

当且仅当 ，

当且仅当 或 ，

当且仅当 。

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

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

模型 <W,R,>，如果对于所有 w ∈W 有 w A，

框架 <W,R>，如果对于 的所有可能的选择，它在 <W,R,> 中是有效的，

框架或模型的类 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 : A → A。T 在任何自反的框架 <W,R> 中是有效的: 如果 w A，则 w A，因为 w R w。在另一方面，使 T 有效的框架必须是自反的: 固定 w ∈W，并定义命题变量 p 的满足为如下: u p 当且仅当 w R u。那么 w p，所以 w p 于 T，这意味着 w R w 使用了 的定义。我们见到 T 对应于自反的 Kripke 框架的类。

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

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

常见模态公理模式

名字	公理	框架条件
T		自反的
4		传递的
D		连续的:
B		对称的
5		欧几里德式的:
GL		R 传递的, R-1 良基的
Grz		R 自反的和传递的, R-1−Id 良基的
H
M		(一个复杂的二阶性质)
G

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

常见正规模态逻辑

名字	公理	框架条件
K	-	所有框架
T	T	自反的
K4	4	传递的
S4	T, 4	预序
S5	T, 5 或 D, B, 4	等价
S4.3	T, 4, H	全序
S4.1	T, 4, M	预序,
S4.2	T, 4, G	有向预序
GL	GL 或 4, GL	有限的严格偏序
Grz, S4Grz	Grz 或 T, 4, Grz	有限的偏序
D	D	连续的
D45	D, 4, 5	传递的、连续的和欧几里德式的

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

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

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

当且仅当对所有的公式 ，如果 则 ，

当且仅当 。

典范模型是 L 的模型，因为所有的 L-MCS 包含 L 的所有定理。通过佐恩引理，每个 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 语义对有多于一个模态的逻辑有直接的推广。带有 作为必然性算子的集合的语言的 Kripke 框架，由对每个 i ∈I 装备上二元关系 R_i 一个非空集合 W构成。满足关系的定义修改为如下:

当且仅当 。

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

当且仅当 。

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

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

直觉 Kripke 模型是一个三元组 ，这里的 是偏序(也有说是预序) Kripke 框架，而 满足下列条件:

如果 是命题变量，，而且 ，则 (单调性要求)，

当且仅当 并且 ，

当且仅当 或者 ，

当且仅当 对于所有 ， 蕴含 ，

当且仅当 没有 ，，

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

设 L 是一阶语言。L 的 Kripke 模型是三元组 <W,≤,{M_w}_w∈W>，这里的 <W,≤> 是直觉 Kripke 框架，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 A[e]:

w P(t₁,...,t_n)[e] 当且仅当 P(t₁[e],...,t_n[e]) 成立于 M_w，

w (A ∧ B)[e] 当且仅当 w A[e] 并且 w B[e]，

w (A ∨ B)[e] 当且仅当 w A[e] 或者 w B[e]，

w (A → B)[e] 当且仅当 对于所有的 u ≥ w，u A[e] 蕴含 u B[e]，

w ¬ A[e] 当且仅当 没有 u ≥ w，u A[e]，

w (∃x A)[e] 当且仅当 存在一个 a ∈M_w，使得 w A[e(x→a)]，

w (∀x A)[e] 当且仅当 对于所有的 u ≥ w 和所有的 a ∈M_u，u A[e(x→a)]。

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

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

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

在 Kripke 语义中天然的同态叫做p-态射(它是伪满射的简写，但这个术语很少用)。Kripke 框架 <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’。

Kripke 模型 <W,R,> 和 <W’,R’,’> 的 p-态射是它们的底层框架的 p-态射 f:W → W’，它满足

对于任何命题变量 p，w p 当且仅当 f(w) ’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 p 当且仅当 w’ ’p。

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

我可以使用拆分(unravelling)把 Kripke 模型变换成树。给出一个模型 <W,R,> 和固定的节点 w₀ ∈ W，我们定义一个模型 <W’,R’,’>，这里的 W’ 是所有有限序列 s=<w₀,w₁,...,w_n> 的集合，使得对于所有 i

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

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

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

f 是满射，

f 保持可及关系，和(在两个方向上)变量 p ∈ X 的满足性，

如果 f(u) R’ f(v) 并且 u A，这里的 A ∈X，则 v A。

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

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

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