直覺主義邏輯的直觀語(yǔ)義與形式語(yǔ)義

1. 直覺主義思想概述

20世紀(jì)初，對(duì)數(shù)學(xué)基礎(chǔ)的研究催生了以荷蘭數(shù)學(xué)家布勞威爾(L.E.J. Brouwer)為代表的直覺主義學(xué)派(intuitionist school)，其思想被稱為直覺主義。(1)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，上海： 上海人民出版社，1989年，第47頁(yè)。直覺主義思想可以追溯到德國(guó)哲學(xué)家康德(I. Kant)的數(shù)學(xué)哲學(xué)立場(chǎng)，布勞威爾稱：“在康德那里，我們發(fā)現(xiàn)了一種古老的直覺主義形式，也就是： 在人類推理中，時(shí)間和空間是作為固有的概念形式，這種觀點(diǎn)在如今卻幾乎完全被拋棄了。對(duì)于康德來(lái)說(shuō)，算術(shù)公理和幾何公理是先驗(yàn)綜合判斷，也就是獨(dú)立于經(jīng)驗(yàn)的判斷并且不能被分析地證明；這就解釋了它們?cè)诮?jīng)驗(yàn)世界中和抽象中都具有的絕對(duì)精確性。因此對(duì)康德來(lái)說(shuō)，算術(shù)律和幾何律在經(jīng)驗(yàn)上不能被證明的這種可能性不僅僅被堅(jiān)定的信念所排除，而且也是完全無(wú)法想象的?！?2)引自L.E.J. Brouwer, Intuitionism and Formalism, (1912A), in Collected Works， I, A. Heyting(ed.), Amsterdam： North-Holland, 1975, p.125。

直覺主義學(xué)派把數(shù)學(xué)理解為人類心智的創(chuàng)造性活動(dòng)，以“存在必須被構(gòu)造”作為它的座右銘，拒斥“實(shí)無(wú)窮”而采納“潛無(wú)窮”觀，并試圖在其哲學(xué)立場(chǎng)基礎(chǔ)上去改造經(jīng)典數(shù)學(xué)。(3)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第47—48頁(yè)。直覺主義學(xué)派對(duì)“構(gòu)造”的理解體現(xiàn)在只接受心智可構(gòu)造的數(shù)學(xué)對(duì)象和數(shù)學(xué)證明。(4)其一，可構(gòu)造的數(shù)學(xué)對(duì)象指的是，對(duì)于所考慮的數(shù)學(xué)對(duì)象來(lái)說(shuō)，我們的心智能夠通過一定的方法能行地(有窮步)得到它們；其二，可構(gòu)造的數(shù)學(xué)證明指的是，對(duì)于一個(gè)數(shù)學(xué)命題來(lái)說(shuō)，我們能夠能行地判定它的真。在對(duì)待邏輯和數(shù)學(xué)的關(guān)系上，直覺主義認(rèn)為： 直覺是數(shù)學(xué)的基礎(chǔ)，邏輯不是數(shù)學(xué)的基礎(chǔ)，邏輯只是數(shù)學(xué)的一部分，邏輯有效性依賴于數(shù)學(xué)的可構(gòu)造性，這也導(dǎo)致了經(jīng)典邏輯中某些邏輯規(guī)律在直覺主義那里不是普遍有效的。(5)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第48頁(yè)。最典型的例子便是經(jīng)典邏輯中的“排中律(law of excluded middle)”在直覺主義那里不是普遍有效的(6)這里，普遍有效指的是無(wú)論在有窮論域還是無(wú)窮論域上都是有效的，直覺主義不接受無(wú)窮論域上的“排中律”，但有窮論域上的“排中律”在直覺主義那里依然是有效的。，進(jìn)而經(jīng)典數(shù)學(xué)中常用的間接證明方法也不能接受。(7)間接證明方法指的是用反證法證明一個(gè)肯定命題，即為了證明一個(gè)肯定命題A為真，可以通過假設(shè)“非A”為真推出矛盾，進(jìn)而證明A為真。布勞威爾在論證排中律在數(shù)學(xué)中不是普遍有效的時(shí)候，提供了一種被稱作“弱反例(weak counterexamples)”的方法： 如果承認(rèn)了排中律普遍有效，那么就能夠得到，某一尚未被證明或否證的數(shù)學(xué)陳述或者能夠證明，或者能夠被否證，換句話說(shuō)，承認(rèn)排中律普遍有效就要承認(rèn)我們能夠確證某一尚未被確證的數(shù)學(xué)陳述。(8)參見L.E.J. Brouwer, The Unreliablity of The Logical Principles, 1908C. in Collected Works I, A. Heyting (ed.), Amsterdam： North—Holland, 1975, pp.109-110。上述那種未被確證的數(shù)學(xué)陳述通常被稱為“弱反例”，我們能夠通過利用尋找“弱反例”的辦法來(lái)論證經(jīng)典邏輯中的某些邏輯規(guī)律不是直覺主義所普遍接受的。

2. 直覺主義邏輯的直觀語(yǔ)義——證明解釋

以下我們僅以直覺主義命題邏輯為例來(lái)闡述直覺主義邏輯的直觀語(yǔ)義(9)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第48—49頁(yè)。：

(1) 對(duì)于一個(gè)原子命題(不含邏輯聯(lián)結(jié)詞的命題)A來(lái)說(shuō)，判定A為真當(dāng)且僅當(dāng)給出A的構(gòu)造性證明。

(3) 對(duì)于合取命題A∧B來(lái)說(shuō)，判定A∧B為真，當(dāng)且僅當(dāng)，同時(shí)給出對(duì)A的構(gòu)造性證明和對(duì)B的構(gòu)造性證明。

(4) 對(duì)于析取命題A∨B來(lái)說(shuō)，判定A∨B為真，當(dāng)且僅當(dāng)，給出對(duì)A的構(gòu)造性證明或?qū)的構(gòu)造性證明；另一種更強(qiáng)的對(duì)析取命題的構(gòu)造性解釋是： 判定A∨B為真，當(dāng)且僅當(dāng)，可指明A,B中哪一個(gè)析取支是正確的，并且給出該析取支的構(gòu)造性證明。(10)參見L. Goble(ed.), The Blackwell Guide to Philosophical Logic, Malden, Mass.: Blackwell Publishers Ltd, 2001, p.224。

(5) 對(duì)于蘊(yùn)涵命題A→B來(lái)說(shuō)，判定A→B為真，當(dāng)且僅當(dāng)，給出一個(gè)構(gòu)造，這個(gè)構(gòu)造使得： 從任何假設(shè)A為真的構(gòu)造都能夠得到對(duì)B的構(gòu)造性證明。

3. 直覺主義邏輯的形式系統(tǒng)

在直覺主義邏輯直觀語(yǔ)義的基礎(chǔ)上，直覺主義邏輯形式系統(tǒng)從語(yǔ)型的視角刻畫了關(guān)于邏輯聯(lián)結(jié)詞和量詞的邏輯規(guī)律。已有的直覺主義命題邏輯的形式系統(tǒng)主要有三種類型： 希爾伯特式(Hilbert-style)系統(tǒng)(也稱公理系統(tǒng))、自然推理(natural deduction)系統(tǒng)和矢列演算(sequent calculus)。容易證明，這三種邏輯形式系統(tǒng)是等價(jià)的，也就是說(shuō)，在同一形式語(yǔ)言下，三種類型的形式系統(tǒng)的內(nèi)定理集是相同的。(11)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第62頁(yè)；馮棉： 《結(jié)構(gòu)推理》，桂林： 廣西師范大學(xué)出版社，2015年，第44頁(yè)。

自然推理系統(tǒng)能夠較好地反映直覺主義構(gòu)造性推理的特性。(12)參見D.M. Gabbay and F. Guenthner(eds.), Handbook of Philosophical Logic(Second Edition), Vol.5, Berlin： Springer Netherlands, 2014. p.10?；诖?，我們以直覺主義命題邏輯的自然推理系統(tǒng)IPN為例(13)見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第51—52頁(yè)。，分析直覺主義邏輯形式系統(tǒng)的特點(diǎn)。

IPN由兩個(gè)部分組成： 一、形式語(yǔ)言；二、推理規(guī)則。

我們先給出形式語(yǔ)言L：

推理規(guī)則有11條：

以下，A,B,C表示任意公式；Γ, Δ, Ω是任意的由公式組成的集合(可為空集?)；├是推演符號(hào)，Γ├A表示以Γ為前提，經(jīng)過有限次使用系統(tǒng)的規(guī)則，得到公式A；如果?├A(可簡(jiǎn)記為├A)，那么稱A是IPN的內(nèi)定理。

規(guī)則1： 如果A∈Γ，那么Γ├A。

規(guī)則2： 如果Γ├A， Δ├B，那么?！圈ぉ?A∧B)。

規(guī)則3： 如果Γ├(A∧B)，那么Γ├A。

規(guī)則4： 如果Γ├(A∧B)，那么Γ├B。

規(guī)則5： 如果Γ├A，那么Γ├(A∨B)。

規(guī)則6： 如果Γ├A，那么Γ├(A∨B)。

規(guī)則7： 如果Γ├(A∨B)，Δ∪{A}├C，Ω∪{B}├C，那么Γ∪Δ∪Ω├C。

規(guī)則8： 如果?！葅A}├B，那么Γ├(A→B)。

規(guī)則9： 如果Γ├A， Δ├(A→B)，那么Γ∪Δ├B。

IPN的11條推理規(guī)則都是遵循直觀語(yǔ)義的，我們以規(guī)則5為例做驗(yàn)證(其他規(guī)則的驗(yàn)證類似)，由于Γ├A，這意味著： 由Γ中的那些公式為前提，可以用構(gòu)造性的方法推出A，根據(jù)析取命題的直觀語(yǔ)義，由A的構(gòu)造性證明可獲得(A∨B)構(gòu)造性證明，進(jìn)而，由Γ中的那些公式出發(fā)，可以用構(gòu)造性的方法推出(A∨B)，即Γ├(A∨B)成立。進(jìn)而，我們可以把IPN的內(nèi)定理理解為直觀語(yǔ)義下的邏輯規(guī)律，即形如定理A的命題都被判定為真，也就是說(shuō)，總能給出對(duì)它的構(gòu)造性證明。

4. 直覺主義邏輯的博弈式語(yǔ)義

雖然直覺主義邏輯形式系統(tǒng)的構(gòu)建是為了從語(yǔ)型角度來(lái)刻畫證明解釋下的邏輯規(guī)律，但就形式系統(tǒng)本身來(lái)說(shuō)，它僅僅是符號(hào)的推演系統(tǒng)，這使得我們可以從不同的語(yǔ)義視角去理解它，進(jìn)而對(duì)邏輯常項(xiàng)(logical constants)的理解也存在多種可能性。博弈式語(yǔ)義(game-theoretical semantics從博弈的視角去理解直覺主義邏輯的形式系統(tǒng)，它以對(duì)話語(yǔ)義(dialogue semantics)為代表，對(duì)話語(yǔ)義利用兩個(gè)主體的博弈來(lái)給出邏輯常項(xiàng)(logical constants)的語(yǔ)義解釋。

以下，我們以直覺主義命題邏輯為例來(lái)分析對(duì)話語(yǔ)義的特點(diǎn)。

我們先給出相關(guān)語(yǔ)型定義(16)參見W. Felscher, “Dialogues, Strategies and Intuitionistic Provability,” Annals of Pure and Applied Logic, Vol.28 (1985): 217-254, at pp.218-219。：

在語(yǔ)言L的基礎(chǔ)上我們?cè)黾铀膫€(gè)初始符號(hào)： ∧1, ∧2,P,O，并增加一個(gè)概念： 特殊符號(hào)(special symbols)，特殊符號(hào)僅可以是： ∧1, ∧2, ∨。公式和特殊符號(hào)都被稱為表達(dá)式(expression)，別無(wú)其他；對(duì)于任意一個(gè)表達(dá)式e，我們可以形成兩個(gè)被標(biāo)記的表達(dá)式Pe(可以直觀理解為： 支持e)和Oe(可以直觀理解為： 反對(duì)e)。如果一個(gè)被標(biāo)記的表達(dá)式是公式，那么它被稱為斷言(assertion)；如果一個(gè)被標(biāo)記的表達(dá)式是特殊符號(hào)，那么它被稱為符號(hào)攻擊(symbolic attack)。X,Y作為變量X≠Y，可取P或Q。

令A(yù),B，A1,A2為任意公式，對(duì)邏輯聯(lián)結(jié)詞的解釋是由論證形式(argumentation form)決定的(17)參見Ibid., p.219，表述有所修改。：

(1)合取聯(lián)結(jié)詞∧的論證形式為： (2) 析取聯(lián)結(jié)詞∨的論證形式為：

斷言：X(A1∧A2) 斷言：X(A1∨A2)

攻擊：Y∧i,i∈{1, 2} 攻擊：Y∨

防守：XAi防守：XAi,i∈{1, 2}

攻擊：YA攻擊：YA

防守：XB防守： 無(wú)

可進(jìn)一步定義“對(duì)話(dialogue)”、“D對(duì)話(D-dialogue)”和“策略(strategy)”等概念。(18)參見Ibid., pp.219-220。(對(duì)于公式A來(lái)說(shuō)，如果存在對(duì)它的策略，那么我們稱公式A是對(duì)話可證的。)

基于對(duì)話語(yǔ)義可以證明IPN的可靠性定理(soundness theorem)和完全性定理(completeness theorem)，也就是說(shuō)，IPN的內(nèi)定理都是對(duì)話可證的公式并且對(duì)話可證的公式都是IPN的內(nèi)定理。(19)參見T. Piecha, Some Notes on Intuitionistic Logic and Dialogue Semantics, Lecture Notes, 2018, p.36。

對(duì)于任意公式A來(lái)說(shuō)，由于對(duì)A的策略是有限長(zhǎng)的并且能夠有限步尋找到對(duì)A的策略，因此對(duì)話語(yǔ)義的構(gòu)建是符合直覺主義思想的。對(duì)話語(yǔ)義在博弈的視角，利用“對(duì)話可證”解讀了直觀語(yǔ)義中“構(gòu)造性證明”這個(gè)概念的內(nèi)涵；同時(shí)，對(duì)話可證的公式從邏輯形式系統(tǒng)的內(nèi)定理得到了刻畫。在這個(gè)意義上，對(duì)話語(yǔ)義可以理解為一種符合直覺主義邏輯直觀語(yǔ)義的形式語(yǔ)義。

5. 直覺主義邏輯的模型論式語(yǔ)義

模型論式語(yǔ)義(model-theoretical semantics)可以理解成集合-關(guān)系語(yǔ)義，這種語(yǔ)義以Kripke語(yǔ)義為代表。以下，我們以直覺主義命題邏輯的Kripke語(yǔ)義為例來(lái)分析：

定義5.1(20)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第70—71頁(yè)。： 系統(tǒng)IPN(21)IPN與直覺主義命題邏輯公理系統(tǒng)IP是等價(jià)的(內(nèi)定理集相同)，進(jìn)而系統(tǒng)IP的Kripke模型與系統(tǒng)IPN的Kripke模型等價(jià)，參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第62頁(yè)。的一個(gè)Kripke模型是一有序三元組〈K,R,V〉，其中K是一非空集合，被稱為結(jié)點(diǎn)集或時(shí)間集，R是K上的滿足自反性(reflexivity)和傳遞性(transitivity)(22)自反性： 對(duì)于任意的x∈K， 〈x， x〉∈R(我們把〈x,x〉∈R記為xRx)；傳遞性： 對(duì)于任意的x,y,z∈K，如果xRy且yRz，那么xRz。的二元關(guān)系(R?K×K)，V是賦值函數(shù)，其定義域?yàn)镕×K(F是所有公式組成的集合)，值域是{1, 0}，V滿足以下五個(gè)條件(以下，A,B是任意公式，變?cè)猭∈K)：

(1)V(pi,k)=1,V(pi,k)=0，兩者有且僅有一個(gè)成立，其中，i是任意正整數(shù)；此外，如果V(pi,k)=1，那么對(duì)于任意的h∈{x|kRx,x∈K}，都有V(pi,h)=1(這個(gè)條件也可以簡(jiǎn)稱為命題變?cè)膯握{(diào)性條件)。

(2)V((A∧B),k)=1，當(dāng)且僅當(dāng)，V(A,k)=1且V(B,k)=1。

(3)V((A∨B),k)=1，當(dāng)且僅當(dāng)，V(A,k)=1或V(B,k)=1。

(4)V((A→B),k)=1，當(dāng)且僅當(dāng)，對(duì)于任意的h∈{x|kRx,x∈K}，都有V(A,h)=0或V(B,h)=1。

(5)V(A,k)=1，當(dāng)且僅當(dāng)，對(duì)于任意的h∈{x|kRx,x∈K}，都有V(A,h)=0。

可以證明，IPN的Kripke模型是存在的。(23)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第70—71頁(yè)。對(duì)于任意的IPN的Kripke模型，命題變?cè)膯握{(diào)性條件可以直接擴(kuò)充到公式的單調(diào)性條件，即： 令A(yù)為任意公式，變?cè)猭∈K，如果V(A,k)=1，那么對(duì)于任意的h∈{x|kRx,x∈K}，都有V(A,h)=1。(24)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第72—73頁(yè)。

定義5.2(25)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第73頁(yè)。： 對(duì)于任意的INP的Kripke模型〈K,R,V〉，如果對(duì)于任意k∈K，都有V(A,k)=1，那么稱A是IPN有效的(也可稱為Kripke有效的)，其中A是任意公式。

從代數(shù)視角來(lái)看，Kripke語(yǔ)義和基于偽布爾代數(shù)(26)也被稱作海廷代數(shù)(Heyting algebras)。(pseudo-Boolean algebras)的代數(shù)語(yǔ)義是等價(jià)的： 一個(gè)公式是Kripke有效的(Kripke valid)，當(dāng)且僅當(dāng)，它是代數(shù)有效的(algebraically valid)。(27)參見M. Fitting, Intuitionistic Logic, Model Theory and Forcing, Amsterdam： North—Holland, 1969, p.27.

基于Kripke語(yǔ)義，可以證明： IPN有可靠性定理和完全性定理，也就是說(shuō)： 對(duì)于任意公式A來(lái)說(shuō)，A是IPN的內(nèi)定理，當(dāng)且僅當(dāng)，A是IPN有效的。(28)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，上海： 上海人民出版社，1989年，第83—84頁(yè)。除此之外，在Kripke樹模型(tree models)基礎(chǔ)上可以證明IPN的有限模型性(finite model property)和析取性質(zhì)(disjunction property)。(29)參見D. Jacquette(ed.), A Companion to Philosophical Logic, Oxford： Blackwell Publishing, 2006, p.525.

根據(jù)定義5.1, Kripke模型的構(gòu)建是基于集合論框架的，是依賴于實(shí)無(wú)窮的；但直覺主義邏輯的直觀語(yǔ)義是遵循直覺主義的哲學(xué)立場(chǎng)的，是拒斥實(shí)無(wú)窮的。在這個(gè)意義上，作為直覺主義邏輯形式系統(tǒng)的形式語(yǔ)義來(lái)說(shuō)，Kripke語(yǔ)義與直覺主義邏輯的直觀語(yǔ)義有偏離的，這是第一種偏離。

根據(jù)定義5.2，公式的IPN有效是根據(jù)賦值函數(shù)V來(lái)定義的，也就是說(shuō)，公式的IPN有效是一種外延定義；而根據(jù)直覺主義邏輯的直觀語(yǔ)義，IPN有效的公式(即IPN的內(nèi)定理)被判定為真是根據(jù)構(gòu)造性證明這個(gè)內(nèi)涵意義來(lái)定義的。在這個(gè)意義下，Kripke語(yǔ)義與直觀語(yǔ)義也是有偏離的，這是第二種偏離。

6. 進(jìn)一步討論

直覺主義邏輯的直觀語(yǔ)義對(duì)構(gòu)造性證明的內(nèi)涵意義的理解可以通過對(duì)蘊(yùn)含式(A→B)的解釋呈現(xiàn)出來(lái)，比如(30)例子參見L. Goble(ed.), The Blackwell Guide to Philosophical Logic, Blackwell Publishers Ltd, 2001. p.225。：

令A(yù)為命題：π的十進(jìn)制展開中出現(xiàn)連續(xù)20個(gè)7；

令B為命題：π的十進(jìn)制展開中出現(xiàn)連續(xù)19個(gè)7，

就Kripke語(yǔ)義而言，雖然它是一種抽象的集合-關(guān)系語(yǔ)義，但我們可以通過對(duì)它作認(rèn)識(shí)論的解釋(作為人的認(rèn)知過程的一種模擬)來(lái)直觀理解它(31)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第69—70頁(yè)。：

時(shí)間集K的元素被解釋為“時(shí)刻(或時(shí)期)”；對(duì)于任意的k1,k2∈K，R(k1,k2)被解釋為“時(shí)刻k2不先于時(shí)刻k1(R自然滿足自反性和傳遞性)”；對(duì)于任意公式A和k∈K，V(A,k)=1被解釋成“命題A在k時(shí)刻被確認(rèn)為真”，相應(yīng)地，V(A,k)=0被解釋成“命題A在k時(shí)刻未被確認(rèn)為真”，公式的單調(diào)性條件告訴我們： 一個(gè)命題在某一時(shí)刻被確認(rèn)為真了，那么在以后的時(shí)刻它依然是被確認(rèn)為真的，這是一種對(duì)真理積累式的認(rèn)知過程。

在這種認(rèn)識(shí)論解釋下，我們能夠更為直觀地闡釋直覺主義邏輯的Kripke語(yǔ)義與直觀語(yǔ)義的偏離：

根據(jù)定義5.1的(4)，“命題(A→B)在時(shí)刻k被確認(rèn)為真”等價(jià)于“對(duì)于時(shí)刻k及未來(lái)任意時(shí)刻h，要么命題A未被確認(rèn)為真，要么命題B被確認(rèn)為真”，進(jìn)而，命題(A→B)在時(shí)刻k是否被確認(rèn)為真就依賴于命題A,B在時(shí)刻k及未來(lái)任意時(shí)刻h上是否被確認(rèn)為真的分布情況。就上面的例子來(lái)說(shuō)，當(dāng)我們把命題A,B放到我們的認(rèn)識(shí)論解釋下來(lái)看，如果B在任意時(shí)刻k被確認(rèn)為真，那么根據(jù)公式的單調(diào)性條件可知： 對(duì)于時(shí)刻k及未來(lái)任意時(shí)刻h，命題B都被確認(rèn)為真，進(jìn)而命題(A→B)都被確認(rèn)為真，也就是說(shuō)，僅僅通過B在時(shí)刻k是否被確認(rèn)為真就能夠判斷命題(A→B)在時(shí)刻k是否被確認(rèn)為真，而不必訴諸于A,B的內(nèi)涵意義，這就與直觀語(yǔ)義對(duì)蘊(yùn)涵的理解有偏離。

雖然存在這種偏離，但是Kripke語(yǔ)義的認(rèn)識(shí)論解釋從認(rèn)識(shí)論的視角對(duì)直覺主義邏輯形式系統(tǒng)作了解讀，豐富了對(duì)它的理解，與對(duì)話語(yǔ)義一起為直覺主義邏輯在其他領(lǐng)域中的應(yīng)用開辟了道路，這也使得直覺主義邏輯可以作為橋梁讓多種不同領(lǐng)域聯(lián)系起來(lái)，促進(jìn)多學(xué)科的交叉研究。

除此之外，Kripke語(yǔ)義為直覺主義邏輯形式系統(tǒng)的元邏輯研究帶來(lái)了便利，比如，利用它可以證明IPN的完全性定理、有限模型性和析取性質(zhì)；由于直覺主義邏輯的直觀語(yǔ)義缺乏對(duì)相關(guān)語(yǔ)義概念的嚴(yán)格定義，因此關(guān)于直覺主義邏輯形式系統(tǒng)的一些好的元性質(zhì)很難從中挖掘出來(lái)。

在Kripke語(yǔ)義基礎(chǔ)上，利用一定的變換，可以得到直覺主義命題邏輯公理系統(tǒng)IP(它等價(jià)于IPN)與模態(tài)命題邏輯系統(tǒng)S4的聯(lián)系，即： 對(duì)于任意公式A，A是IP的內(nèi)定理，當(dāng)且僅當(dāng)，A的S4變換式是S4的內(nèi)定理(32)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第97—101頁(yè)。。與強(qiáng)調(diào)內(nèi)涵意義的直覺主義邏輯直觀語(yǔ)義相比，Kripke語(yǔ)義體現(xiàn)了在外延層面建立直覺主義邏輯和其他非經(jīng)典邏輯之間的聯(lián)系的優(yōu)勢(shì)。