Kripke框架

**克里普克語義**(也叫做**關係語義**或**框架語義**，並經常混淆於可能世界語義) 是模態邏輯系統的形式語義，於 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_1⊆_L_2 是對應於同一個框架類的正規模態邏輯，_L_1 不證明 _L_2 的所有定理。那麼 _L_1 是克里普克不完備的。例如，模式 $\Box (A\equiv \Box A)\to \Box A$ 生成一個不完備的邏輯，因為它對應於同 _GL_ 一樣的框架類 (viz. 傳遞性和逆良基的框架)，但是它不證明 $\Box A\to \Box \Box A$ 。

在下表中給出常見模態公理和它們對應的類的列表。注意：公理的名字經常是多變的。

下面是一些常見正規模態邏輯系統的列表。對於其中一些的框架條件是簡化了的：邏輯關於在表中給出的框架類是_完備的_，但是它們可能_對應_於更大的一類框架。

### 典範模型

對於任何正規模態邏輯 _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_ 裝備上二元關係 _Ri_ 一個非空集合 _W_ 構成。滿足關係的定義修改為如下:

　
: $w\Vdash \Box _{i}A$ 若且唯若 $\forall u\,(w\;R_{i}\;u\Rightarrow u\Vdash A)$ 。

由 Tim Carlson 發現的簡化的語義，經常用於多模態可證明性邏輯。**Carlson 模型**是結構 <_W_,_R_,{_Di_}i∈_I_,⊩>，帶有一個單一的可及關係 _R_，和給每個模態的子集 _Di_ ⊆ _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_,≤,{_Mw_}w∈_W_>，這裡的 <_W_,≤> 是直覺克里普克框架，_Mw_ 是 _w_ ∈_W_ 每個節點的 (經典) _L_- 結構，而下列相容性條件只要在 _u_ ≤ _v_ 時都是成立的:

* _Mu_ 的域包含在 _Mv_ 的域中，
* _Mu_ 和 _Mv_ 中的函數符號實現一致於 _Mu_ 的元素，
* 對於每個 _n_ 元謂詞 _P_ 和元素 _a_1,...,_an_ ∈_Mu_: 如果 _P_(_a_1,...,_an_) 成立於 _Mu_，則它成立於 _Mv_。

給出經由 _Mw_ 的元素的變量求值 _e_，我們定義滿足關係 _w_  $\Vdash $ _A_[_e_]:

* _w_  $\Vdash $ _P_(_t_1,...,_tn_)[_e_] 若且唯若 _P_(_t_1[_e_],...,_tn_[_e_]) 成立於 _Mw_，
* _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_ ∈_Mw_，使得 _w_  $\Vdash $ _A_[_e_(_x_→_a_)]，
* _w_  $\Vdash $ (∀_x_ _A_)[_e_] 若且唯若 對於所有的 _u_ ≥ _w_ 和所有的 _a_ ∈_Mu_，_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_0 ∈ _W_，我們定義一個模型 <_W’_,_R’_, $\Vdash $ ’>，這裡的 _W’_ 是所有有限序列 _s_=<_w_0,_w_1,...,_wn_> 的集合，使得對於所有 _i_<_n_ 和 _s_  $\Vdash $ _p_，_wi_ _R_ _wi+1_ 若且唯若對於所有變量 _p_，_wn_  $\Vdash $ _p_。定義可及關係 _R’_ 變化；在最簡單的情況下我們置

　
: <_w_0,_w_1,...,_wn_> _R’_ <_w_0,_w_1,...,_wn_,_wn+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.