1. 直覺主義思想概述

20世紀(jì)初，對數(shù)學(xué)基礎(chǔ)的研究催生了以荷蘭數(shù)學(xué)家布勞威爾(L.E.J. Brouwer)為代表的直覺主義學(xué)派(intuitionist school)，其思想被稱為直覺主義。(1)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，上海： 上海人民出版社，1989年，第47頁。直覺主義思想可以追溯到德國哲學(xué)家康德(I. Kant)的數(shù)學(xué)哲學(xué)立場，布勞威爾稱：“在康德那里，我們發(fā)現(xiàn)了一種古老的直覺主義形式，也就是： 在人類推理中，時間和空間是作為固有的概念形式，這種觀點(diǎn)在如今卻幾乎完全被拋棄了。對于康德來說，算術(shù)公理和幾何公理是先驗(yàn)綜合判斷，也就是獨(dú)立于經(jīng)驗(yàn)的判斷并且不能被分析地證明；這就解釋了它們在經(jīng)驗(yàn)世界中和抽象中都具有的絕對精確性。因此對康德來說，算術(shù)律和幾何律在經(jīng)驗(yàn)上不能被證明的這種可能性不僅僅被堅定的信念所排除，而且也是完全無法想象的。”(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)造性活動，以“存在必須被構(gòu)造”作為它的座右銘，拒斥“實(shí)無窮”而采納“潛無窮”觀，并試圖在其哲學(xué)立場基礎(chǔ)上去改造經(jīng)典數(shù)學(xué)。(3)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，第47—48頁。直覺主義學(xué)派對“構(gòu)造”的理解體現(xiàn)在只接受心智可構(gòu)造的數(shù)學(xué)對象和數(shù)學(xué)證明。(4)其一，可構(gòu)造的數(shù)學(xué)對象指的是，對于所考慮的數(shù)學(xué)對象來說，我們的心智能夠通過一定的方法能行地(有窮步)得到它們；其二，可構(gòu)造的數(shù)學(xué)證明指的是，對于一個數(shù)學(xué)命題來說，我們能夠能行地判定它的真。在對待邏輯和數(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頁。最典型的例子便是經(jīng)典邏輯中的“排中律(law of excluded middle)”在直覺主義那里不是普遍有效的(6)這里，普遍有效指的是無論在有窮論域還是無窮論域上都是有效的，直覺主義不接受無窮論域上的“排中律”，但有窮論域上的“排中律”在直覺主義那里依然是有效的。，進(jìn)而經(jīng)典數(shù)學(xué)中常用的間接證明方法也不能接受。(7)間接證明方法指的是用反證法證明一個肯定命題，即為了證明一個肯定命題A為真，可以通過假設(shè)“非A”為真推出矛盾，進(jìn)而證明A為真。布勞威爾在論證排中律在數(shù)學(xué)中不是普遍有效的時候，提供了一種被稱作“弱反例(weak counterexamples)”的方法： 如果承認(rèn)了排中律普遍有效，那么就能夠得到，某一尚未被證明或否證的數(shù)學(xué)陳述或者能夠證明，或者能夠被否證，換句話說，承認(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é)陳述通常被稱為“弱反例”，我們能夠通過利用尋找“弱反例”的辦法來論證經(jīng)典邏輯中的某些邏輯規(guī)律不是直覺主義所普遍接受的。

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

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

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

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

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

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

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

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

自然推理系統(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頁。，分析直覺主義邏輯形式系統(tǒng)的特點(diǎn)。

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

我們先給出形式語言L：

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

以下，A,B,C表示任意公式；Γ, Δ, Ω是任意的由公式組成的集合(可為空集?)；├是推演符號，Γ├A表示以Γ為前提，經(jīng)過有限次使用系統(tǒng)的規(guī)則，得到公式A；如果?├A(可簡記為├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，那么?！圈ぁ圈俯繡。

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

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

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

4. 直覺主義邏輯的博弈式語義

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

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

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

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

令A(yù),B，A1,A2為任意公式，對邏輯聯(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防守： 無

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

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

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

5. 直覺主義邏輯的模型論式語義

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

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

(1)V(pi,k)=1,V(pi,k)=0，兩者有且僅有一個成立，其中，i是任意正整數(shù)；此外，如果V(pi,k)=1，那么對于任意的h∈{x|kRx,x∈K}，都有V(pi,h)=1(這個條件也可以簡稱為命題變元的單調(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)，對于任意的h∈{x|kRx,x∈K}，都有V(A,h)=0或V(B,h)=1。

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

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

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

從代數(shù)視角來看，Kripke語義和基于偽布爾代數(shù)(26)也被稱作海廷代數(shù)(Heyting algebras)。(pseudo-Boolean algebras)的代數(shù)語義是等價的： 一個公式是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語義，可以證明： IPN有可靠性定理和完全性定理，也就是說： 對于任意公式A來說，A是IPN的內(nèi)定理，當(dāng)且僅當(dāng)，A是IPN有效的。(28)參見馮棉： 《經(jīng)典邏輯與直覺主義邏輯》，上海： 上海人民出版社，1989年，第83—84頁。除此之外，在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í)無窮的；但直覺主義邏輯的直觀語義是遵循直覺主義的哲學(xué)立場的，是拒斥實(shí)無窮的。在這個意義上，作為直覺主義邏輯形式系統(tǒng)的形式語義來說，Kripke語義與直覺主義邏輯的直觀語義有偏離的，這是第一種偏離。

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

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

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

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

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

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

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

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

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

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

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

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