關係語義

克里普克語義( 嘛是叫做關係語義抑是框架語義，並經過定定咧透濫可能世界語義 ) 是模態邏輯系統的形式語義，佇咧一九五空年代的暗期佮一九六空年代早期由索爾・阿倫・克里普克伊的建立。伊後來為另外一个非經典邏輯，上重要的直覺邏輯所接受。克里普克語義的發現是非經典邏輯開發中重大突破，因為這款邏輯的模型論佇克里普克進前實際上是不存在的。

模態邏輯的語義

對咱的目的，模態邏輯的語言由命題變量，讀者佮意的布爾連結詞的完備集合 ( 比如講 { → , ¬ } 抑是 { ∨ , ∧ , ¬ } )，佮模態算子 $ \ 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 $。

佇下表中予出常見模態公理佮𪜶對應的類的列表。注意：公理的名不時是多變的。

下底是一寡捷看著正規模態邏輯系統的列表。對其中的一寡框殼條件是較簡化的：邏輯關於佇表中予出的框殼類是 _ 完備的 _，猶毋過𪜶可能就 _ 對應 _ 佇閣較大的一類框殼。

典範模型

對任何正規模的邏輯 _ 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 _、_ 四 _、_ D _、_ B _、_ 五 _、_ H _、_ G _ ( 和𪜶的任意組合 ) 攏是典範的。_ GL _ 和 _ Grz _ 毋是典範的，因為𪜶是無影蓋絚。公理 _ M _ 家己毋是規範的 ( Goldblatt , 一千九百九十一 )，但是組合的邏輯 _ S 四配一 _ ( 事實上甚至 _ K 四配一 _ ) 是典範的。

一般的，予定的公理敢是典範的敢是會當判定的。毋過咱知影一个好的充分條件 : H。Sahlqvist 熟似別了遮爾仔廣泛的一類公式 ( 這馬叫做 Sahlqvist 公式 )

Sahlqvist 公式是典範的，
對應於 Sahlqvist 公式的框架類是一階可定義的，
有計算對一个予定的 Sahlqvist 公式的對應框架條件的算法。

這是一个非常強力的準則；比如講，頂懸列出的典範的所有公理是實際上的 ( 等價於 ) Sahlqvist 公式。

有限模型的性質

邏輯有有限模型的性質( FMP )，如果伊若是有限框架的類是完備的。這个概念的主要應用之一是可判定性問題：伊服從 Post 定理，有 FMP 的交歸公理化的模態邏輯 _ L _ 是會當判定的，準若予定的有限框架是毋是 _ L _ 的模型是會當判定的。特別是，有 FMP 的所有的有限可公理化的邏輯攏是會當判定的。

有各種方法共定做一个邏輯建立 FMP。精練閣擴展規範模型構造通常就會用得矣，使用工具若過濾抑是拆分。閣有一種可能性，予免切的相繼式演算的完備性證明通常直接產生有限模型。

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

佇某一寡狀況下，阮會使用 FMP 來證明邏輯的克里普克完備性：所有正規模的邏輯因為模態代數的類攏是完備的，而且 _ 有限的 _ 模態代數會當變換做克里普克框架。做例，Robert Bull 使用這个方法證明矣 _ S 四配三 _ 的所有的普通擴展攏有 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 _ 一 , . . . , _ an _ ∈ _ Mu _ : 若是 _ P _ ( _ a _ 一 , . . . , _ an _ ) 成立於 _ Mu _，著伊成立佇 _ Mv _。

予出經由 _ Mw _ 元素的變量求值 _ e _，咱定義滿足關係的 _ w _ $ \ Vdash $ _ A _ [_ e _] :

_ w _ $ \ Vdash $ _ P _ ( _ t _ 一 , . . . , _ tn _ ) [_ e _] 若是唯一 _ P _ ( _ t _ 一 [_ 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 語義

成做獨立開發的層論的一部份，佇一九六五年左右捌著克里普克語義密切相關於佇 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 _ 一 , . . . , _ wn _ > 的集合，予對所有 _ i _ < _ n _ 和 _ s _ $ \ Vdash $ _ p _，_ wi _ _ R _ _ wi + 一 _ 若是唯若對所有變量 _ p _，_ wn _ $ \ Vdash $ _ p _。定義會當佮關係 _ R’_ 變化；佇上蓋簡單的情形下阮置

< _ w _ 零 , _ w _ 一 , . . . , _ wn _ > _ R’_ < _ w _ 零 , _ w _ 一 , . . . , _ wn _ , _ wn + 一 _ > ,

但是真濟應用需要這个關係的自反佮 / 抑是傳達閉包，抑是類似的變更加。

過濾是 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 , 兩千空一 .
Basic Modal Logic. R . A . Bull and K . Segerberg . In _ The Handbook of Philosophical Logic , _ volume 二 , pages 一-鋪八十八 . Kluwer , 一千九百八十四 .
_ A New Introduction to Modal Logic _ . G . E . Hughes , M . J . Cresswell . Routledge , 九百九十六 .
_ Modal Logic _ . A . Chagrov , M . Zakharyaschev . Oxford University Press , 一千九百九十七 .
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 . 一 ( 五鋪六 ) : 三百空九九三百九十二 , 兩千空三 .
Intuitionistic Logic. D . van Dalen . In _ The Handbook of Philosophical Logic , _ volume 三 , pages 兩百二十五-被三百三十九 . Reidel , 一千九百八十六 .
_ Elements of Intuitionism _ . M . Dummett . Clarendon Press , 一千九百七十七 .
_ Intuitionistic Logic , Model Theory and Forcing _ . M . Fitting . North-Holland , 一千九百六十九 .
_ Sheaves in Geometry and Logic _ . S . Mac Lane and I . Moerdijk . Springer-Verlag , 一千九百九十一 .

參見

克里普克結構
會當有關係

外部連結

_ Introduction to Mathematical Logic _ by Drs . Detlovs and Podnieks . Chapter 四 , Section 四 : " Constructive Propositional Logic—Kripke Semantics " .
_ Kripke Models _ , a Word document by John P . Burgess .