關係語義

克里普克語義(也叫做關係語義或框架語義，並經常混淆於可能世界語義)是模態邏輯系統的形式語義，於 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.