必威电竞|足球世界杯竞猜平台

來源：互聯網

Kripke 語義（也叫做關系語義或框架語義，并經常混淆于可能世界語義）是模態邏輯系統的形式語義，于 1950 年代晚期和 1960 年代早期由 Saul Kripke 建立。它后來為另一個非經典邏輯，最重要的直覺邏輯所接受。Kripke 語義的發現是非經典邏輯開發中重大突破，因為這種邏輯的模型論在 Kripke 之前實際上是不存在的。

模態邏輯語義

對于我們的目的，模態邏輯的語言由命題變量，讀者喜歡的布爾連結詞的完備集合(比如 {→,￢} 或 {∨,∧,￢})，和模態算子□ (“必然性”)構成。對偶的模態算子◇A(“可能性”) 定義為一個簡寫：◇A=￢□￢A。更多背景請參見模態邏輯。

基本定義

Kripke 框架或模態框架是 對，這里的 W 是非空集合，R 是在 W 上的二元關系。W 的元素叫做節點或世界，而 R 叫做可及關系。

Kripke 模型是 \Vdash> 三元組，這里的 是 Kripke 框架，而 $\backslash Vdash$ 是在 W 的節點和模態公式之間的如下關系:

$w\backslash Vdash\backslash neg\; A$ 當且僅當 $w\backslash not\backslash Vdash\; A$，

$w\backslash Vdash\; A\backslash to\; B$ 當且僅當 $w\backslash not\backslash Vdash\; A$ 或 $w\backslash Vdash\; B$，

$w\backslash Vdash\backslash Box\; A$ 當且僅當 $\backslash forall\; u\backslash ,(w\backslash ;\; R\backslash ;\; u\; \backslash Rightarrow\; u\backslash Vdash\; A)$。

我們把 w $\backslash Vdash$A 讀做“w 滿足 A”，“A 滿足于 w”，或“w 力迫 A”。關系 $\backslash Vdash$ 叫做“滿足關系”、“求值關系”或“力迫關系”。注意滿足關系由它在命題變量上的值唯一確定。

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

模型 \Vdash>，如果對于所有 w ∈W 有 w $\backslash Vdash$A，

框架 ，如果對于 $\backslash 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 : $\backslash Box$A → A。T 在任何自反的框架 中是有效的: 如果 w $\backslash Vdash\; \backslash Box$A，則 w $\backslash Vdash$A，因為 w R w。在另一方面，使 T 有效的框架必須是自反的: 固定 w ∈W，并定義命題變量 p 的滿足為如下: u $\backslash Vdash$p 當且僅當 w R u。那么 w $\backslash Vdash\; \backslash Box$p，所以 w $\backslash Vdash$p 于 T，這意味著 w R w 使用了 $\backslash Vdash$ 的定義。我們見到 T 對應于自反的 Kripke 框架的類。

特征化 L 的對應類經常比證明它的完備性要容易許多，所以對應性充當完備性證明的指導。對應性還用于證實模態邏輯的不完備性: 假定 L1?L2 是對應于同一個框架類的正規模態邏輯，L1 不證明 L2 的所有定理。那么 L1 是 Kripke 不完備的。例如，模式 $\backslash Box(A\backslash equiv\backslash Box\; A)\backslash to\backslash Box\; A$ 生成一個不完備的邏輯，因為它對應于同 GL 一樣的框架類(viz. 傳遞性和逆良基的框架)，但是它不證明 $\backslash Box\; A\backslash to\backslash Box\backslash Box\; A$。

規范模型

概述

對于任何正規模態邏輯 L，我們可以構造一個 Kripke 模型(稱為規范模型)，它且只有它使 L 的定理有效，通過接納使用極大一致集合作為模型的標準技術。規范 Kripke 模型扮演的角色類似于在代數語義中的 Lindenbaum–Tarski代數構造。

公式集合

L是一致的，如果從它們、L 的公理和肯定前件中不能推導出矛盾。極大 L一致的集合(簡寫為 L-MCS)是沒有真L一致的超集的 L一致的集合。

L 的規范模型是 Kripke 模型 \Vdash>，這里的 W 是所有L-MCS，而關系 R 和 $\backslash Vdash$ 為如下:

$X\backslash ;R\backslash ;Y$ 當且僅當對所有的公式 $A$，如果 $\backslash Box\; A\backslash in\; X$ 則 $A\backslash in\; Y$，

$X\backslash Vdash\; A$ 當且僅當 $A\backslash 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 公式)

蛛網膜下腔出血lqvist 公式是規范的，

對應于 Sahlqvist 公式的框架類是一階可定義的，

有計算對一個給定的 Sahlqvist 公式的對應框架條件的算法。

這是一個非常強力的準則；例如，上面列出的規范的所有公理是實際上的(等價于) Sahlqvist 公式。

有限模型性質

概述

邏輯擁有有限模型性質(FMP)，如果它關于有限框架的類是完備的。這個概念的主要應用之一是可判定性問題: 它服從 Post 定理，有 FMP 的遞歸公理化的模態邏輯 L 是可判定的，倘若給定的有限框架是否是 L 的模型是可判定的。特別是，有 FMP 的所有的有限可公理化的邏輯都是可判定的。

有各種方法為給定的邏輯建立 FMP。精練并擴展規范模型構造通常就行了，使用工具如過濾或拆分。還有一種可能性，給予免切的相繼式演算的完備性證明通常直接產生有限模型。

多數實際上使用的模態系統(包括所有上面列出的)都有 FMP。

在某些情況下，我們可以使用 FMP 來證明邏輯的 Kripke 完備性: 所有正規模態邏輯關于模態代數的類都是完備的，而有限的模態代數可以變換成 Kripke 框架。作為例子，Robert Bull 使用這個方法證明了 S4.3 的所有普通擴展都有 FMP，并且是 Kripke 完備的。

多模態邏輯

Kripke 語義對有多于一個模態的邏輯有直接的推廣。帶有 $\backslash \{\backslash Box\_i;\backslash ,i\backslash in\; I\backslash \}$ 作為必然性算子的集合的語言的 Kripke 框架，由對每個 i ∈I 裝備上二元關系 Ri 一個非空集合 W構成。滿足關系的定義修改為如下:

$w\backslash Vdash\backslash Box\_i\; A$ 當且僅當 $\backslash forall\; u\backslash ,(w\backslash ;R\_i\backslash ;u\backslash Rightarrow\; u\backslash Vdash\; A)$。

由 Tim Carlson 發現的簡化的語義，經常用于多模態可證明性邏輯。Carlson 模型是結構 ，帶有一個單一的可及關系 R，和給每個模態的子集 Di ? W。滿足性定義為

$w\backslash Vdash\backslash Box\_i\; A$ 當且僅當 $\backslash forall\; u\backslash in\; D\_i\backslash ,(w\backslash ;R\backslash ;u\backslash Rightarrow\; u\backslash Vdash\; A)$。

Carlson 模型比通常的多模態 Kripke 模型易于形象化和使用；但是，Kripke 完備的多模態邏輯是 Carlson 不完備的。

直覺邏輯

直覺邏輯的 Kripke 語義服從和模態邏輯的語義同樣的原理，但是它使用了滿足的不同的定義。

直覺

Kripke 模型是一個三元組 \Vdash>，這里的 是傳遞的和自反的 Kripke 框架(就是說可及關系是預序)，而 $\backslash Vdash$ 滿足下列條件:

如果 p 是命題變量，w ≤ u，而且 w $\backslash Vdash$p，則 u $\backslash Vdash$p (堅持條件)，

w $\backslash Vdash$A ∧ B 當且僅當 w $\backslash Vdash$A 并且 w $\backslash Vdash$B，

w $\backslash Vdash$A ∨ B 當且僅當 w $\backslash Vdash$A 或者 w $\backslash Vdash$B，

w $\backslash Vdash$A → B 當且僅當對于所有 u ≥ w，u $\backslash Vdash$A 蘊含 u $\backslash Vdash$B，

無 w $\backslash 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 $\backslash Vdash$A[e]:

w $\backslash Vdash$P(t1,...,tn)[e] 當且僅當 'P(t1[e],...,tn[e]) 成立于 Mw，

w $\backslash Vdash$(A ∧ B)[e] 當且僅當 w $\backslash Vdash$A[e] 并且 w $\backslash Vdash$B[e]，

w $\backslash Vdash$(A ∨ B)[e] 當且僅當 w $\backslash Vdash$A[e] 或者 w $\backslash Vdash$B[e]，

w $\backslash Vdash$(A → B)[e] 當且僅當對于所有的 u ≥ w，u $\backslash Vdash$A[e] 蘊含 u $\backslash Vdash$B[e]，

無 w $\backslash Vdash$⊥[e]，

w $\backslash Vdash$(?x A)[e] 當且僅當存在一個 a ∈Mw，使得 w $\backslash Vdash$A[e(x→a)]，

w $\backslash Vdash$(?x A)[e] 當且僅當對于所有的 u ≥ w 和所有的 a ∈Mu，u $\backslash Vdash$A[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 $\backslash Vdash$p 當且僅當 f(w) $\backslash 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 $\backslash Vdash$p 當且僅當 w’ $\backslash Vdash$’p。

從這個定義我們得到的關鍵性質是模型的雙仿(所以也是 p-態射)保持所有公式的滿足性，而不只是命題變量。

我可以使用拆分(unravelling)把 Kripke 模型變換成樹。給出一個模型 \Vdash> 和固定的節點 w0 ∈ W，我們定義一個模型 \Vdash’>，這里的 W’ 是所有有限序列 s= 的集合，使得對于所有 i\Vdashp，wi R wi+1 當且僅當對于所有變量 p，wn $\backslash Vdash$p。定義可及關系 R’ 變化；在最簡單的情況下我們置

R’ ,

但是很多應用需要這個關系的自反與/或傳遞閉包，或類似的變更。

過濾是 p-態射的一個變種。設 X 是在采納子公式(subformulas)下閉合的公式的集合。模型 \Vdash> 的 X-過濾是從W 到模型 \Vdash’> 的映射 f，使得

f 是滿射，

f 保持可及關系，和(在兩個方向上)變量 p ∈ X 的滿足性，

如果 f(u) R’ f(v) 并且 u $\backslash Vdash\; \backslash Box$A，這里的 $\backslash Box$A ∈X，則 v $\backslash Vdash$A。

得到了 f 保持來自 X 的所有公式的滿足性。在典型的應用中，我們把 f 采納為在W 在下列關系上對份額的投影

u ≡X v 當且僅當對于所有 A ∈X，u $\backslash Vdash$A 當且僅當 v $\backslash Vdash$A。

同在拆分的情況下一樣，定義可及關系在份額變化上。

歷史和術語

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 語義，因為這是對先驅們做的重要貢獻的失禮。反對另一個最廣泛使用的術語可能世界語義的理由是它不適合應用于不是可能性和必然性的模態，比如在認識或道義邏輯中。他們喜歡術語關系語義或框架語義。

參考資料 >