關係語義檢視原始碼討論檢視歷史

關係語義

原圖鏈接

中文名: 關係語義 外文名: Kripke 別 名: 框架語義 建立時間: 1950年代晚期 創始人: Saul Kripke 混 淆: 可能世界語義 性 質: 模擬邏輯語義

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

模態邏輯語義

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

基本定義

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

Kripke 模型是 <W,R,<math>\Vdash</math>> 三元組，這裡的 <W,R> 是 Kripke 框架，而 <math>\Vdash</math> 是在 W 的節點和模態公式之間的如下關係:

<math>w\Vdash\neg A</math> 當且僅當 <math>w\not\Vdash A</math>，

<math>w\Vdash A\to B</math> 當且僅當 <math>w\not\Vdash A</math> 或 <math>w\Vdash B</math>，

<math>w\Vdash\Box A</math> 當且僅當 <math>\forall u\,(w\; R\; u \Rightarrow u\Vdash A)</math>。

我們把 w <math>\Vdash</math>A 讀做 「w 滿足 A」，「A 滿足於 w」，或 「w 力迫 A」。關係 <math>\Vdash</math> 叫做「滿足關係」、「求值關係」或「力迫關係」。注意滿足關係由它在命題變量上的值唯一確定。

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

模型 <W,R,<math>\Vdash</math>>，如果對於所有 w ∈W 有 w <math>\Vdash</math>A，

框架 <W,R>，如果對於 <math>\Vdash</math> 的所有可能的選擇，它在 <W,R,<math>\Vdash</math>> 中是有效的，

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

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

規範模型

概述

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

公式集合

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

L 的規範模型是 Kripke 模型 <W,R,<math>\Vdash</math>>，這裡的 W 是所有L-MCS，而關係 R 和 <math>\Vdash</math> 為如下:

<math>X\;R\;Y</math> 當且僅當對所有的公式 <math>A</math>，如果 <math>\Box A\in X</math> 則 <math>A\in Y</math>，

<math>X\Vdash A</math> 當且僅當 <math>A\in X</math>。

規範模型

規範模型是 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 語義對有多於一個模態的邏輯有直接的推廣。帶有 <math>\{\Box_i;\,i\in I\}</math> 作為必然性算子的集合的語言的 Kripke 框架，由對每個 i ∈I 裝備上二元關係 Ri 一個非空集合 W構成。滿足關係的定義修改為如下:

<math>w\Vdash\Box_i A</math> 當且僅當 <math>\forall u\,(w\;R_i\;u\Rightarrow u\Vdash A)</math>。

由 Tim Carlson 發現的簡化的語義，經常用於多模態可證明性邏輯。Carlson 模型是結構 <W,R,i∈I,⊩>，帶有一個單一的可及關係 R，和給每個模態的子集 Di ⊆ W。滿足性定義為

<math>w\Vdash\Box_i A</math> 當且僅當 <math>\forall u\in D_i\,(w\;R\;u\Rightarrow u\Vdash A)</math>。

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

直覺邏輯

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

直覺

Kripke 模型是一個三元組 <W,≤,<math>\Vdash</math>>，這裡的 <W,≤> 是傳遞的和自反的 Kripke 框架(就是說可及關係是預序)，而 <math>\Vdash</math> 滿足下列條件:

如果 p 是命題變量，w ≤ u，而且 w <math>\Vdash</math>p，則 u <math>\Vdash</math>p (堅持條件)，

w <math>\Vdash</math>A ∧ B 當且僅當 w <math>\Vdash</math>A 並且 w <math>\Vdash</math>B，

w <math>\Vdash</math>A ∨ B 當且僅當 w <math>\Vdash</math>A 或者 w <math>\Vdash</math>B，

w <math>\Vdash</math>A → B 當且僅當對於所有 u ≥ w，u <math>\Vdash</math>A 蘊含 u <math>\Vdash</math>B，

無 w <math>\Vdash</math>⊥。

直覺邏輯關於它的 Kripke 語義是可靠的和完備的，並且它有 FMP。

直覺一階邏輯

設 L 是一階語言。L 的 Kripke 模型是三元組 <W,≤,w∈W>，這裡的 <W,≤> 是直覺 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 <math>\Vdash</math>A[e]:

w <math>\Vdash</math>P(t1,...,tn)[e] 當且僅當 'P(t1[e],...,tn[e]) 成立於 Mw，

w <math>\Vdash</math>(A ∧ B)[e] 當且僅當 w <math>\Vdash</math>A[e] 並且 w <math>\Vdash</math>B[e]，

w <math>\Vdash</math>(A ∨ B)[e] 當且僅當 w <math>\Vdash</math>A[e] 或者 w <math>\Vdash</math>B[e]，

w <math>\Vdash</math>(A → B)[e] 當且僅當對於所有的 u ≥ w，u <math>\Vdash</math>A[e] 蘊含 u <math>\Vdash</math>B[e]，

無 w <math>\Vdash</math>⊥[e]，

w <math>\Vdash</math>(∃x A)[e] 當且僅當存在一個 a ∈Mw，使得 w <math>\Vdash</math>A[e(x→a)]，

w <math>\Vdash</math>(∀x A)[e] 當且僅當對於所有的 u ≥ w 和所有的 a ∈Mu，u <math>\Vdash</math>A[e(x→a)]。

這裡的 e(x→a) 是給予 x 值 a 的求值，在其他方面一致於 e。

Kripke-Joyal 語義

作為獨立開發的層論的一部分，在 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,<math>\Vdash</math>> 和 <W』,R』,<math>\Vdash</math>』> 的 p-態射是它們的底層框架的 p-態射 f:W → W』，它滿足

對於任何命題變量 p，w <math>\Vdash</math>p 當且僅當 f(w) <math>\Vdash</math>』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 <math>\Vdash</math>p 當且僅當 w』 <math>\Vdash</math>』p。

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

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

<w0,w1,...,wn> R』 <w0,w1,...,wn,wn+1>,

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

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

f 是滿射，

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

如果 f(u) R』 f(v) 並且 u <math>\Vdash \Box</math>A，這裡的 <math>\Box</math>A ∈X，則 v <math>\Vdash</math>A。

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

u ≡X v 當且僅當對於所有 A ∈X，u <math>\Vdash</math>A 當且僅當 v <math>\Vdash</math>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 語義，因為這是對先驅們做的重要貢獻的失禮。反對另一個最廣泛使用的術語可能世界語義的理由是它不適合應用於不是可能性和必然性的模態，比如在認識或道義邏輯中。他們喜歡術語關係語義或框架語義。

如何理解Kripke semantics？

Kripke semantics也可以叫做可能世界語義學。原始的思想是：Kripke model上的每個點代表一個可能世界。Kripke semantics會用在很多地方。就模態邏輯（描述「必然」「可能」的邏輯）來說，Kripke model上會有一個二元關係R，這個R的直觀含義是：如果xRy這個二元關係成立，那麼意味着在x這個世界上看，y是有可能發生的。於是，如果一個命題「P」在所有可能的情況下都成立，那麼「必然P」就成立。在每個人的不同的視角看來，對於「什麼是有可能的什麼是不可能的」會產生不同的判斷。這就好比在Kripke model中，每個可能世界出發能夠通過二元關係R到達的可能世界集合是不同的。即，有些可能世界上看P是必然的，有些則認為P是不必然的。當然，Kripke語義還用在很多不同的地方。這裡限於篇幅就不展開了。我在2017年發表的關於分離邏輯（Separation logic）的工作就是用Kripke semantics統一了各種看似不相兼容的分離邏輯的語義。