程華清

1 引言

對邱奇-費(fèi)奇悖論1邱奇-費(fèi)奇悖論指的是：在“任意命題的真都可能被知道”和“存在不知道的真命題”的前提下，通過經(jīng)典的模態(tài)和認(rèn)知邏輯推演會導(dǎo)致結(jié)論“任意命題的真都被知道”，這違背了我們的直覺。（Church-Fitch paradox）的解悖促進(jìn)了直覺主義認(rèn)知邏輯的研究。直覺主義認(rèn)知邏輯是基于直覺主義邏輯的認(rèn)知擴(kuò)充，直覺主義邏輯的構(gòu)建遵循Brouwer-Heyting-Kolmogrov 解釋2簡稱BHK 解釋。BHK 解釋是從構(gòu)造性語境下對邏輯算子的解釋，關(guān)于BHK 解釋的詳細(xì)闡釋見本文第二節(jié)。，這意味著直覺主義邏輯包含認(rèn)知因素3直覺主義把數(shù)學(xué)理解為心智的構(gòu)造性活動(dòng)，這可被視作一種認(rèn)知活動(dòng)，直覺主義邏輯是直覺主義數(shù)學(xué)的衍生品，更多闡釋詳見文中第二節(jié)內(nèi)容。，但其形式語言中不含認(rèn)知算子，而直覺主義認(rèn)知邏輯的形式語言能夠表達(dá)含有認(rèn)知算子K的公式KA，對認(rèn)知算子的不同理解形成了不同的直覺主義認(rèn)知邏輯。

直覺主義認(rèn)知邏輯的研究當(dāng)前可分為兩條進(jìn)路：

(1) 接納知識的事實(shí)性（factivity of knowledge）原則KA →A，它也被稱為反射（reflection）原則。這方面的代表是[9]中所構(gòu)建的系統(tǒng)IKT*，構(gòu)建IKT*不依賴于BHK 解釋，而是基于以下觀點(diǎn)：

真在于證實(shí)（verification）的可能性，其中“證實(shí)”被理解為實(shí)時(shí)（real time）呈現(xiàn)給一個(gè)真實(shí)主體（real subject）的事物，但真僅僅需要這樣事物的可能性而不是其實(shí)際的出現(xiàn)。（[9]，第63 頁）

(2) 接納真的構(gòu)造性（constructivity of truth）原則A →KA，它也被稱為余反射（coreflection）原則。這方面的代表是[1]中所構(gòu)建的系統(tǒng)IEL，對IEL 的構(gòu)建旨在遵循BHK 解釋，并持有觀點(diǎn)：

直覺主義認(rèn)知狀態(tài)（信念或知識）是證實(shí)的結(jié)果，其中“證實(shí)”指的是足以達(dá)到實(shí)際目的而給出的確鑿的（conclusive）證據(jù)（evidence）。4這種對“證實(shí)”的理解與[9]中所理解的“證實(shí)”稍有不同，參見[1]中第288 頁的注釋30。（[1]，第269 頁）

由此可見，[1]試圖從直覺主義原初立場出發(fā)來建立關(guān)于直覺主義知識的邏輯，這是[9]未考慮的。如[1]中所述：

因此威廉姆森（Williamson）的直覺主義認(rèn)知邏輯沒有表達(dá)基于BHK的知識（BHK-based knowledge）的含義（而這是我們的目標(biāo)），與此同時(shí)它也把經(jīng)典的認(rèn)知假設(shè)引入到直覺主義的語境中來。（[1]，第288 頁）

S.Artemov 將命題KA解讀為“A是直覺主義知識”，并借助“證實(shí)”的概念給出認(rèn)知算子K 的預(yù)期理解。（[1]）IEL 接受直覺主義反射（intuitionistic reflection）原則KA →??A，它被視作直覺主義知識的真值條件（truth condition）。

Artemov 的工作具有啟發(fā)性，它為回到直覺主義本身來發(fā)展（模態(tài)）認(rèn)知邏輯提供了基本思路（比如[7]對IEL 做了一般化的研究，證明了IEL 能夠嵌入到其S5 類型系統(tǒng)中），進(jìn)而促進(jìn)了直覺主義認(rèn)識論（intuitionistic epistemology）的研究。遺憾的是，IEL 的預(yù)期解釋并未嚴(yán)格遵循BHK 解釋，導(dǎo)致IEL 的構(gòu)建未達(dá)到預(yù)期目標(biāo)，本文第二節(jié)會對此作詳細(xì)的論證。第三節(jié)簡要回顧IEL 的形式化工作，并在第二節(jié)討論基礎(chǔ)上重新理解IEL。第四節(jié)提出了KA的新解讀，并由此引出直覺主義真和經(jīng)典真之間不同程度的真，在此基礎(chǔ)上重新理解IEL 系統(tǒng)的一些重要內(nèi)定理。最后在第五節(jié)提出IEL 系統(tǒng)對應(yīng)問題的一個(gè)猜測。

2 IEL 的預(yù)期解釋與BHK 解釋的偏離

IEL 的構(gòu)建試圖遵循BHK 解釋，但這種嘗試有一定局限性，本節(jié)從直覺主義視角下邏輯和數(shù)學(xué)的關(guān)系出發(fā)來論證：IEL 的預(yù)期解釋偏離了BHK 解釋，進(jìn)而IEL 并未達(dá)到預(yù)期構(gòu)建目標(biāo)。

BHK 解釋是直覺主義對基本邏輯聯(lián)結(jié)詞和量詞的標(biāo)準(zhǔn)解釋，它經(jīng)由布勞威爾（L.E.J.Brouwer）、海廷（A.Heyting）和柯爾莫哥洛夫（A.Kolmogorov）發(fā)展而來?；具壿嬄?lián)結(jié)詞的BHK 解釋如下所述（[8]，第9 頁）：

(H1)A ∧B的一個(gè)證明（proof）通過呈現(xiàn)A的一個(gè)證明和B的一個(gè)證明而得到。

(H2)A ∨B的一個(gè)證明通過呈現(xiàn)A的一個(gè)證明或B的一個(gè)證明而得到，此外規(guī)定：所呈現(xiàn)的證明就作為A ∨B的證明。

(H3)A →B的一個(gè)證明是一個(gè)構(gòu)造（construction），這個(gè)構(gòu)造使得我們能夠從A的任意證明轉(zhuǎn)換為B的一個(gè)證明。

(H4) 荒謬（absurdity）⊥（矛盾）沒有證明。?A的一個(gè)證明是一個(gè)構(gòu)造，這個(gè)構(gòu)造將A的任意假設(shè)的證明轉(zhuǎn)換為矛盾的一個(gè)證明。

不難發(fā)現(xiàn)，BHK 解釋規(guī)定了一個(gè)復(fù)合命題的證明是以何種方式從它的子命題的證明而獲得，不過其核心在于對證明和構(gòu)造的理解，如[8]中所言：

BHK 解釋自身沒有解釋力（explanatory power）：一個(gè)有效的經(jīng)典邏輯模式被視作構(gòu)造地不可接受的，這完全取決于對“構(gòu)造”“函數(shù)”“運(yùn)算”的解釋。（[8]，第33 頁）

在BHK 解釋中，證明和構(gòu)造指的都是心智的構(gòu)造5可稱其為構(gòu)造性證明，它可被理解為直觀的能行（effective）方法。（mental constructions，[6]，第87 頁）。這種對證明和構(gòu)造的理解基于直覺主義對數(shù)學(xué)以及數(shù)學(xué)和邏輯關(guān)系的獨(dú)特理解：

（一）直覺主義把數(shù)學(xué)理解為心智的構(gòu)造性活動(dòng)，這意味著直覺主義只接受心智可構(gòu)造的數(shù)學(xué)對象和心智可構(gòu)造的數(shù)學(xué)證明，即：數(shù)學(xué)對象能夠通過直觀能行的方法得到，數(shù)學(xué)命題所表達(dá)的內(nèi)容能夠通過直觀能行的方法直接驗(yàn)證。數(shù)學(xué)定理表達(dá)的是純粹經(jīng)驗(yàn)的事實(shí)，數(shù)學(xué)不能建立在公理化基礎(chǔ)之上，直覺（intuition）就是數(shù)學(xué)可靠性的基礎(chǔ)。直覺主義數(shù)學(xué)的代表是選擇序列（choice sequences）理論，利用選擇序列能夠遵循直覺主義思想構(gòu)造連續(xù)統(tǒng)（continuum），形象地說，可以利用選擇序列把連續(xù)統(tǒng)“算術(shù)化”，進(jìn)而發(fā)展直覺主義分析學(xué)。

（二）數(shù)學(xué)不依賴于語言，語言僅僅是記錄數(shù)學(xué)構(gòu)造的工具，邏輯是利用語言記錄數(shù)學(xué)構(gòu)造所產(chǎn)生的形式規(guī)律，它的有效性自然依賴于數(shù)學(xué)的構(gòu)造性。邏輯可以看作是數(shù)學(xué)的應(yīng)用，如[6]所述：

邏輯可被視作語言學(xué)的一部分或者關(guān)于世界的哲學(xué)理論，在這兩種理解下它都屬于應(yīng)用數(shù)學(xué)。僅僅第三種解釋處于純數(shù)學(xué)討論范圍內(nèi)。邏輯定理是數(shù)學(xué)定理。邏輯不是數(shù)學(xué)的基礎(chǔ)，恰恰相反，在概念上它是數(shù)學(xué)的復(fù)雜而精細(xì)的部分。（[6]，第86-87 頁）

綜上所述，對構(gòu)造性證明的要求是BHK 解釋的核心，這是由直覺主義邏輯依賴于直覺主義數(shù)學(xué)所決定的。

由于對數(shù)學(xué)的理解不同，導(dǎo)致直覺主義意義上的“真”有別于經(jīng)典意義上的“真”。經(jīng)典意義下，一個(gè)命題的真獨(dú)立于對它的證明；但是在直覺主義看來，一個(gè)數(shù)學(xué)命題被判定為直覺主義真就意味著這個(gè)命題獲得構(gòu)造性證明。

例1.簡單命題“1+12”被判定為直覺主義真，其構(gòu)造性證明為：我們的心智先構(gòu)造出一個(gè)自然數(shù)1，接著再構(gòu)造出一個(gè)自然數(shù)1，之后把這整個(gè)過程與對自然數(shù)2 的構(gòu)造作比較，能夠得出兩者是一樣的。

例2.蘊(yùn)涵命題“如果π的十進(jìn)制展開中出現(xiàn)連續(xù)20 個(gè)7，那么π的十進(jìn)制展開中會出現(xiàn)連續(xù)19 個(gè)7”被判定為直覺主義真，其構(gòu)造性證明為：假設(shè)a是“π的十進(jìn)制展開中出現(xiàn)連續(xù)20 個(gè)7”的任意構(gòu)造性證明，顯然能夠給出一個(gè)構(gòu)造使得從a得到“π的十進(jìn)制展開中出現(xiàn)連續(xù)19 個(gè)7”的構(gòu)造性證明。（[5]，第225 頁）

基于“直覺主義知識是證實(shí)的結(jié)果”和基本邏輯聯(lián)結(jié)詞的BHK 解釋，[1]在構(gòu)建IEL 時(shí)通過“證實(shí)”概念定義了“命題KA的證明”：KA的一個(gè)證明指的是證實(shí)“A有證明”的確鑿證據(jù)，其中對“A有證明”的證實(shí)無需包含A的證明。6比如基于零知識協(xié)議的證實(shí)便是這類證實(shí)：零知識協(xié)議是一類密碼協(xié)議，通常是概率性的，證明者利用這種協(xié)議能夠使得驗(yàn)證者確信一個(gè)給定命題為真，而無需提供任何額外有用的信息。在此基礎(chǔ)上，反射原則KA →A不被IEL 接受。（[1]，第273-274 頁）（[1]，第270 頁）這個(gè)定義是有缺陷的：根據(jù)前面的闡釋，對構(gòu)造性證明的要求是BHK 解釋的核心，而命題KA的證明并沒有對構(gòu)造性證明的要求，這偏離了BHK解釋的初衷。從另一角度來說，直覺主義數(shù)學(xué)的數(shù)學(xué)對象都是從自然數(shù)出發(fā)而構(gòu)造性得到的（[10]，第47-48 頁），直覺主義數(shù)學(xué)命題是關(guān)于直覺主義數(shù)學(xué)對象的命題，直覺主義邏輯依賴于直覺主義數(shù)學(xué)，上述對“命題KA的證明”的定義超出了直覺主義數(shù)學(xué)的考慮范圍，無法嚴(yán)格遵循BHK 解釋。盡管[1]中對此作了一定辯護(hù)：

反對的要點(diǎn)在于BHK 解釋不能容納非數(shù)學(xué)命題。然而這很清楚是錯(cuò)誤的，因?yàn)樵贐HK 解釋的表述中沒有特別數(shù)學(xué)化的東西，它并未提到數(shù)、函數(shù)、集合、范疇、類型等等。（[1]，第290 頁）

但這段辯護(hù)并不成立，因?yàn)樗袯HK 解釋獨(dú)立于直覺主義數(shù)學(xué)來看待，并未抓住“直覺主義邏輯依賴于直覺主義數(shù)學(xué)”這點(diǎn)。

Artemov 在構(gòu)建IEL 時(shí)主張“直覺主義真蘊(yùn)涵直覺主義知識”：從BHK 解釋出發(fā)，命題A是直覺主義真意味著A獲得證明，證明是一種證實(shí)，由于直覺主義知識是證實(shí)的結(jié)果，因此直覺主義真蘊(yùn)涵直覺主義知識，進(jìn)而余反射原則A →KA被IEL 接受。（[1]，第266-267 頁）但是IEL 所接受的余反射原則A →KA僅僅適用于A是數(shù)學(xué)命題的情況：當(dāng)A是數(shù)學(xué)命題時(shí)，A中不含認(rèn)知算子K，對于任意假設(shè)的A的證明p，由于證明是最嚴(yán)格意義上的證實(shí)，因此p可以作為確鑿的證據(jù)證實(shí)“A有證明”，進(jìn)而KA獲得證明；（[1]，第271 頁）當(dāng)A中包含認(rèn)知算子K時(shí)（不妨令A(yù)為KB），A的真僅僅意味著對A的證實(shí)，并未體現(xiàn)對構(gòu)造性證明的要求（構(gòu)造性證明一定是證實(shí)，而證實(shí)不一定是構(gòu)造性證明），這時(shí)“命題A為真”要弱于“A是直覺主義真”。同樣的道理，對于IEL 所接受的直覺主義反射原則KA →??A來說，它也僅僅適用于A是數(shù)學(xué)命題的情況。

當(dāng)A是不含認(rèn)知算子K的公式時(shí)，余反射原則和直覺主義反射原則可以分別解讀為“直覺主義真蘊(yùn)涵直覺主義知識”以及“直覺主義知識蘊(yùn)涵經(jīng)典真”，可合并簡記為“直覺主義真直覺主義知識經(jīng)典真”。（[1]，第268 頁）此時(shí)可以對A作BHK 解釋，但是BHK 解釋無法擴(kuò)展到含有認(rèn)知算子K的公式上，因?yàn)橐坏┌袯HK 解釋擴(kuò)展到認(rèn)知算子K上，那么就沒辦法保證對構(gòu)造性證明的要求。

綜上所述，IEL 的預(yù)期解釋偏離了BHK 解釋，進(jìn)而構(gòu)建IEL 的預(yù)期目標(biāo)并未達(dá)到。

3 IEL 的形式化工作

本節(jié)簡要回顧IEL 的形式化工作，并在第二節(jié)的討論基礎(chǔ)上重新理解IEL。

令LK為IEL 的形式語言，LK的初始符號由以下部分構(gòu)成：

? 命題變元：p1,p2,p3,...；

? 邏輯聯(lián)結(jié)詞：否定詞?、合取詞∧、析取詞∨和蘊(yùn)含詞→；

? 認(rèn)知算子K；

? 左、右括號：(和)。

初始符號中的四個(gè)邏輯聯(lián)結(jié)詞是相互獨(dú)立的，公式的遞歸定義遵循認(rèn)知邏輯的一般定義方式，在公式省略括號時(shí)，邏輯聯(lián)結(jié)詞以及認(rèn)知算子的聯(lián)結(jié)強(qiáng)度遵循認(rèn)知邏輯通常的約定。

對IEL 的構(gòu)建可采用[2]中使用的直覺主義命題邏輯公理系統(tǒng)（記為IPC）為基礎(chǔ)（[2]，第219-220 頁），在LK語言下對IPC 做認(rèn)知擴(kuò)充。在LK語言下，IEL通過在IPC 基礎(chǔ)上添加如下三條認(rèn)知公理模式而得到（[1]，第276 頁）：

? 分配（distribution）公理模式：K(A →B)→(KA →KB)

? 余反射公理模式：A →KA

? 直覺主義反射公理模式：KA →??A

值得一提的是，[2]對正規(guī)（normal）直覺主義模態(tài)邏輯的模型論研究為直覺主義認(rèn)知邏輯的模型論研究奠定了技術(shù)性基礎(chǔ)。[2]對含有模態(tài)算子□的正規(guī)直覺主義模態(tài)命題邏輯系統(tǒng)HK□做了研究，給出了相應(yīng)的克里普克語義，并保持了直覺主義命題邏輯的基本模型論性質(zhì)。

在HK□的克里普克語義中（[2]，第222 頁），H□框架（frame）是三元有序組〈W,RI,RM〉，其中W是非空集合，RI是W上滿足自反性和傳遞性的二元關(guān)系，RM是W上的另一個(gè)二元關(guān)系，RM和RI要滿足條件：RIRM ?RMRI（RIRM表示集合{〈x,y〉 |存在z，使得xRIz并且zRMy，x,y,z ∈W}，集合RMRI的定義類同）。

單調(diào)性（monotonicity）作為直覺主義邏輯的重要模型論性質(zhì)，不僅在H□框架下的模型依舊保持著，而且[2]中證明了：RM和RI滿足條件RIRM ?RMRI是H□框架下的模型滿足單調(diào)性的充分必要條件（[2]，第223 頁），這個(gè)結(jié)論為構(gòu)造不同的直覺主義認(rèn)知邏輯形式系統(tǒng)的克里普克語義提供了幫助。

Artemov 中構(gòu)造了IEL 的克里普克語義并給出了IEL 模型的認(rèn)識論解釋（[1]，第279-280 頁）：

（一）首先，IEL 模型指的是四元有序組〈W,R,E,V〉，其中〈W,R,V〉是IPC的克里普克模型，即：〈W,R〉是非空偏序（partial order），W被稱為結(jié)點(diǎn)集，其中的元素被稱為結(jié)點(diǎn)，W上的二元關(guān)系R被稱為W 上的“認(rèn)知”關(guān)系，?是命題變元在W上的滿足單調(diào)性的賦值（evaluation）7對于任意結(jié)點(diǎn)w 和任意命題變元p 來說，w ?p 也被稱為“w 力迫（forces）p”。。其次，W上的二元關(guān)系E被稱為W上的“知識”關(guān)系，E滿足：(1)對于任意的結(jié)點(diǎn)u，E(u)?R(u)成立8E(x)表示{x | wEx,x ∈W}，R(x)表示{x | wRx,x ∈W}。；(2) 如果結(jié)點(diǎn)u和v滿足關(guān)系uRv，那么E(v)?E(u) 成立；(3) 對任意的結(jié)點(diǎn)u，E(u)。最后，將賦值?從命題變元（以遞歸定義的方式）擴(kuò)展到合取式A ∧B、析取式A ∨B、蘊(yùn)涵式A →B、否定式?A和認(rèn)知公式KA上，其中對KA的擴(kuò)展定義為：令u是任意的結(jié)點(diǎn)，u?A當(dāng)且僅當(dāng)對于任意的v ∈E(u)都有v?A成立。

在直覺主義命題邏輯克里普克模型的認(rèn)識論解釋9直覺主義命題邏輯克里普克模型的認(rèn)識論解釋參見[10]中第69-70 頁?；A(chǔ)上，IEL 模型的認(rèn)識論解釋為：W和R分別被理解為時(shí)間點(diǎn)組成的集合以及時(shí)間點(diǎn)的先后關(guān)系，對任意時(shí)間點(diǎn)w和v，wRv意為v不先于w。對任意時(shí)間點(diǎn)u，E(u)被理解為u 的“檢查”（audit）集（其中的元素可被稱為“檢查點(diǎn)”）：在“檢查”集的每個(gè)檢查點(diǎn)對命題A的證實(shí)都可能發(fā)生。E滿足的條件(1)被理解為：每個(gè)時(shí)間點(diǎn)u的檢查點(diǎn)v都不先于u，這意味著每個(gè)時(shí)間點(diǎn)的檢查點(diǎn)都只能是該時(shí)間點(diǎn)或該時(shí)間點(diǎn)之后的時(shí)間點(diǎn)。E滿足的條件(2)被理解為：對每個(gè)不先于時(shí)間點(diǎn)u的時(shí)間點(diǎn)v來說，v的檢查點(diǎn)都是u的檢查點(diǎn)，這意味著隨著時(shí)間的流逝，每個(gè)時(shí)間點(diǎn)的檢查點(diǎn)數(shù)是不會增加的。E滿足的條件(3)被理解為：每個(gè)時(shí)間點(diǎn)u都有檢查點(diǎn)。最后，KA的賦值擴(kuò)展定義被理解為：在時(shí)間點(diǎn)u確認(rèn)KA為真（確認(rèn)A是直覺主義知識）當(dāng)且僅當(dāng)在u的“檢查”集中的每個(gè)檢查點(diǎn)都確認(rèn)命題A為真。

（二）“IEL 有效”的概念被定義為：令A(yù)是任意的LK公式，對任意的IEL模型M來說，如果對于任意的結(jié)點(diǎn)w，都有w?A，那么稱A是模型M有效的；如果對任意的IEL 模型M都有：A是模型M有效的，那么稱A是IEL 有效的。

由于R是偏序關(guān)系，因此它自然滿足自反性和傳遞性，以下證明：E和R滿足條件RE ?ER，進(jìn)而可知：若將IEL 模型中的K替換為□，并將R、E分別替換為RI、RM，就成了一個(gè)H□模型。

E和R滿足條件RE ?ER的證明：對任意的結(jié)點(diǎn)w和v，假設(shè)wREv成立，那么存在結(jié)點(diǎn)t使得wRt并且tEv。根據(jù)E滿足的條件(2)可知：由wRt成立和tEv成立可得wEv成立。再根據(jù)R的自反性可知vRv成立，進(jìn)而wERv成立。

在IEL 的克里普克語義基礎(chǔ)上，直覺主義命題邏輯的基本模型論性質(zhì)單調(diào)性、可靠性、完全性和析取性質(zhì)（disjunction property）在IEL 中依然保持著。（[1]，第280-281、283 頁）

IEL 有如下一些重要內(nèi)定理，其中A是任意的LK公式，比如（[1]，第276-277、第282 頁）：

? 定理一“知識的真值條件”?K(A ∧?A)

? 定理二“知識的真值條件”?(KA ∧?A)

? 定理三“知識的真值條件”?A →?KA

? 定理四K?A →?A

另外，利用IEL 模型能夠證明：K(A ∨B)→(KA ∨KB)和KA →A都不是IEL 的內(nèi)定理。（[1]，第281-282 頁）

根據(jù)第二節(jié)的討論，在BHK 解釋基礎(chǔ)上，IEL 預(yù)期解釋中的“命題KA的證明”定義需要修改為：當(dāng)A是數(shù)學(xué)命題時(shí)，KA的一個(gè)“證明”指的是證實(shí)“A有構(gòu)造性證明”的確鑿證據(jù)，其中對“A有構(gòu)造性證明”的證實(shí)無需包含A的構(gòu)造性證明，進(jìn)而KA被判定為真意味著“A是直覺主義真”獲得證實(shí)。盡管IEL預(yù)期解釋借助了BHK 解釋的框架，由于KA的“證明”沒有對構(gòu)造性證明的要求，因此只有不含認(rèn)知算子K的IEL 公式才能在直觀上遵循BHK 解釋；此外有些IEL 公式也無法遵循IEL 的預(yù)期解釋，比如KKp1→KKKp1。把IEL 系統(tǒng)三個(gè)公理模式以及定理一到定理四中的公式A和B都限定在不含認(rèn)知算子K的情況時(shí)，它們在IEL 的預(yù)期解釋下普遍成立。IEL 系統(tǒng)形式語義的建立能夠幫助證明一些公式不是IEL 系統(tǒng)的內(nèi)定理，比如K(A ∨B)→(KA ∨KB)和KA →A；當(dāng)其中的A和B不含認(rèn)知算子K時(shí)，它們在IEL 的預(yù)期解釋下不是普遍成立的。

4 KA 的新解讀及不同程度的真

在IEL 的預(yù)期解釋中，當(dāng)A是不含認(rèn)知算子K的數(shù)學(xué)命題時(shí)，除了可以把KA解讀為“A是直覺主義知識”或“直覺主義知識A獲得證實(shí)”以外，還可以將其理解為“知道‘A是直覺主義真（A獲得構(gòu)造性證明）或A是經(jīng)典真’”，其中聯(lián)結(jié)“A是直覺主義真”和“A是經(jīng)典真”的析取詞“或”是經(jīng)典意義下的析取10這個(gè)析取是元語言，而非IEL 的形式語言。。值得注意的是，這種新解讀已經(jīng)不再堅(jiān)持直覺主義立場了。

在這樣的解讀下，“KA為真”（即“‘知道A’為真”）也是一種介于直覺主義真和經(jīng)典真之間的真，并且聯(lián)系了直覺主義真和經(jīng)典真，即滿足如下關(guān)系：

A是直覺主義真知道“A是直覺主義真或A是經(jīng)典真”（后面對KA的這種解讀中，引號將省略）。A是經(jīng)典真。

詳細(xì)來說，如果A是直覺主義真，那么意味著A獲得了構(gòu)造性證明，由A的構(gòu)造性證明可以知道A是直覺主義真，進(jìn)而知道A是直覺主義真或A是經(jīng)典真；如果知道A是直覺主義真或A是經(jīng)典真，那么一定知道A是經(jīng)典真（A是直覺主義真A是經(jīng)典真），因此A是經(jīng)典真（如果A為假，那么就不可能知道A為真）。上述關(guān)系進(jìn)一步可以擴(kuò)展為：

A是直覺主義真知道A是直覺主義真知道A是直覺主義真或A是經(jīng)典真知道A是經(jīng)典真A是經(jīng)典真。

再反過來考慮上述關(guān)系，不難發(fā)現(xiàn)，如果A是經(jīng)典真，那么不一定知道A是經(jīng)典真；如果知道A是經(jīng)典真，那么一定知道A是直覺主義真或A是經(jīng)典真；如果知道A是直覺主義真或A是經(jīng)典真，那么不一定知道A是直覺主義真；如果知道A是直覺主義真，那么A是直覺主義真。最后產(chǎn)生如下關(guān)系：

A是直覺主義真??知道A是直覺主義真知道A是直覺主義真或A是經(jīng)典真??知道A是經(jīng)典真A是經(jīng)典真。從上述關(guān)系可知，在經(jīng)典視角下，直覺主義真和經(jīng)典真之間產(chǎn)生了三種不同程度的真：

強(qiáng)“A是直覺主義真”“知道A是直覺主義真”

中“知道A是直覺主義真或A是經(jīng)典真”“知道A是經(jīng)典真”

弱“A是經(jīng)典真”

當(dāng)KA被解讀為“知道A是直覺主義真”時(shí)，根據(jù)上述關(guān)系，直覺主義知識坍塌為直覺主義真。以下我們僅考慮在KA被解讀為“知道A是直覺主義真或A是經(jīng)典真”和“知道A是經(jīng)典真”時(shí)，如何重新理解IEL 系統(tǒng)的一些重要內(nèi)定理。需要注意的是，以下公式A和B都不含認(rèn)知算子，它們被理解為任意的數(shù)學(xué)命題，并遵循BHK 解釋。

4.1 KA 被解讀為“知道A 是直覺主義真或A 是經(jīng)典真”的情況

“余反射公理模式”A →KA被解讀為：如果A是直覺主義真，那么知道A是直覺主義真或A是經(jīng)典真。其中聯(lián)結(jié)A和KA的蘊(yùn)涵詞是經(jīng)典蘊(yùn)涵。根據(jù)不同程度真的關(guān)系，A →KA在這種解讀下是普遍成立的。

“直覺主義反射公理模式”KA →??A被解讀為：如果知道A是直覺主義真或A是經(jīng)典真，那么A不可能沒有構(gòu)造性證明。其中聯(lián)結(jié)KA和??A的蘊(yùn)涵詞是經(jīng)典蘊(yùn)涵。KA →??A在這種解讀下是普遍成立的：假設(shè)知道A是直覺主義真或A是經(jīng)典真，那么A是經(jīng)典真，進(jìn)而A可能有構(gòu)造性證明，A沒有構(gòu)造性證明就是不可能的。

“分配公理模式”K(A →B)→(KA →KB)被解讀為：如果知道A →B是直覺主義真或A →B是經(jīng)典真，那么若知道A是直覺主義真或A是經(jīng)典真，則知道B是直覺主義真或B是經(jīng)典真。其中聯(lián)結(jié)K(A →B)和(KA →KB)的蘊(yùn)涵詞以及聯(lián)結(jié)KA和KB的蘊(yùn)含詞都是經(jīng)典蘊(yùn)涵。K(A →B)→(KA →KB)在這種解讀下是普遍成立的：假設(shè)知道A →B是直覺主義真或A →B是經(jīng)典真，那么知道A →B是經(jīng)典真；再假設(shè)知道A是直覺主義真或A是經(jīng)典真，同理得到知道A是經(jīng)典真，進(jìn)而知道B是經(jīng)典真，因此知道B是直覺主義真或B是經(jīng)典真。

“知識的真值條件”?K(A ∧?A)被解讀為：不知道矛盾是直覺主義真或矛盾是經(jīng)典真。其中聯(lián)結(jié)K(A∧?A)的否定詞是經(jīng)典否定。在這種解讀下?K(A∧?A)是普遍成立的：假設(shè)知道矛盾是直覺主義或矛盾是經(jīng)典真，那么矛盾就是經(jīng)典真，而矛盾恒假，所以假設(shè)不成立。

“知識的真值條件”?(KA ∧?A)被解讀為：并非不僅知道A是直覺主義真或A是經(jīng)典真，而且?A是直覺主義真。其中聯(lián)結(jié)(KA ∧?A)的否定詞是經(jīng)典否定，聯(lián)結(jié)KA和?A的合取詞是經(jīng)典合取。在這種解讀下?(KA ∧?A)是普遍成立的：假設(shè)知道A是直覺主義真或A是經(jīng)典真，而且?A是直覺主義真，那么A是經(jīng)典真，進(jìn)而A可能有構(gòu)造性證明，同時(shí)A沒有構(gòu)造性證明，所以假設(shè)不成立。

“知識的真值條件”?A →?KA被解讀為：如果A沒有構(gòu)造性證明，那么不知道A是直覺主義真或A是經(jīng)典真。其中聯(lián)結(jié)?A和?KA的蘊(yùn)涵詞是經(jīng)典蘊(yùn)涵，聯(lián)結(jié)KA的否定詞是經(jīng)典否定。在這種解讀下?A →?KA是普遍成立的：假設(shè)A沒有構(gòu)造性證明，如果知道A是直覺主義真或A是經(jīng)典真，那么A就是經(jīng)典真，進(jìn)而A可能有構(gòu)造性證明，因此不知道A是直覺主義真或A是經(jīng)典真。

定理四K?A →?A被解讀為：如果知道?A是直覺主義真或?A是經(jīng)典真，那么A沒有構(gòu)造性證明。其中聯(lián)結(jié)K?A和?A的蘊(yùn)涵詞是經(jīng)典蘊(yùn)涵。在這種解讀下K?A →?A是普遍成立的：假設(shè)知道?A是直覺主義真或?A是經(jīng)典真，那么A沒有構(gòu)造性證明或A為假，進(jìn)而A沒有構(gòu)造性證明。

最后考察對K(A ∨B)→(KA ∨KB)和KA →A的理解。

K(A ∨B)→(KA ∨KB)被解讀為：如果知道A ∨B是直覺主義真或A ∨B是經(jīng)典真，那么要么知道A是直覺主義真或A是經(jīng)典真，要么知道B是直覺主義真或B是經(jīng)典真。其中聯(lián)結(jié)K(A ∨B)和(KA ∨KB)的蘊(yùn)涵詞是經(jīng)典蘊(yùn)涵，聯(lián)結(jié)KA和KB的析取詞是經(jīng)典析取。在這種解讀下K(A ∨B)→(KA ∨KB)不是普遍成立的：令A(yù)是黎曼猜想（Riemann hypothesis），B為?A，即可得到反例。

KA →A被解讀為：如果知道A是直覺主義真或A是經(jīng)典真，那么A就是直覺主義真。其中聯(lián)結(jié)KA和A的蘊(yùn)涵詞是經(jīng)典蘊(yùn)涵。在這種解讀下KA →A不是普遍成立的：令A(yù)是關(guān)于正整數(shù)的命題“如果m和n是任意正整數(shù)，那么存在正整數(shù)k使得k×m ≥n”11這個(gè)命題也被稱為正整數(shù)的阿基米德性質(zhì)（Archimedean property）。，使用正整數(shù)的最小自然數(shù)原理，通過反證法可以證明A成立（A是經(jīng)典真），進(jìn)而知道A是經(jīng)典真，因此也知道A是直覺主義真或A是經(jīng)典真，但是并未給出A的構(gòu)造性證明。

4.2 KA 被解讀為“知道A 是經(jīng)典真”的情況

“余反射公理模式”A →KA被解讀為：如果A是直覺主義真，那么知道A是經(jīng)典真。其中聯(lián)結(jié)A和KA的蘊(yùn)涵詞是經(jīng)典蘊(yùn)涵。根據(jù)不同程度真的關(guān)系，A →KA在這種解讀下是普遍成立的。

“直覺主義反射公理模式”KA →??A被解讀為：如果知道A是經(jīng)典真，那么A不可能沒有構(gòu)造性證明。其中聯(lián)結(jié)KA和??A的蘊(yùn)涵詞是經(jīng)典蘊(yùn)涵。KA →??A在這種解讀下是普遍成立的：假設(shè)知道A是經(jīng)典真，那么A是經(jīng)典真，進(jìn)而A可能有構(gòu)造性證明，A沒有構(gòu)造性證明就是不可能的。

“分配公理模式”K(A →B)→(KA →KB)被解讀為：如果知道A →B是經(jīng)典真，那么若知道A是經(jīng)典真，則知道B是經(jīng)典真。其中聯(lián)結(jié)K(A →B)和(KA →KB)的蘊(yùn)涵詞以及聯(lián)結(jié)KA和KB的蘊(yùn)含詞都是經(jīng)典蘊(yùn)涵。容易證明K(A →B)→(KA →KB)在這種解讀下是普遍成立的。

“知識的真值條件”?K(A ∧?A)被解讀為：不知道矛盾是經(jīng)典真。其中聯(lián)結(jié)K(A ∧?A)的否定詞是經(jīng)典否定。容易證明在這種解讀下?K(A ∧?A)是普遍成立的。

“知識的真值條件”?(KA ∧?A)被解讀為：并非不僅知道A是經(jīng)典真，而且?A是直覺主義真。其中聯(lián)結(jié)(KA ∧?A)的否定詞是經(jīng)典否定，聯(lián)結(jié)KA和?A的合取詞是經(jīng)典合取。在這種解讀下?(KA ∧?A)是普遍成立的：假設(shè)知道A是經(jīng)典真，而且?A是直覺主義真，那么A可能有構(gòu)造性證明，同時(shí)A沒有構(gòu)造性證明，所以假設(shè)不成立。

“知識的真值條件”?A →?KA被解讀為：如果A沒有構(gòu)造性證明，那么不知道A是經(jīng)典真。其中聯(lián)結(jié)?A和?KA的蘊(yùn)涵詞是經(jīng)典蘊(yùn)涵，聯(lián)結(jié)KA的否定詞是經(jīng)典否定。在這種解讀下?A →?KA是普遍成立的：假設(shè)A沒有構(gòu)造性證明，如果知道A是經(jīng)典真，那么A就是經(jīng)典真，進(jìn)而A可能有構(gòu)造性證明，因此不知道A是經(jīng)典真。

定理四K?A →?A被解讀為：如果知道?A是經(jīng)典真，那么A沒有構(gòu)造性證明。其中聯(lián)結(jié)K?A和?A的蘊(yùn)涵詞是經(jīng)典蘊(yùn)涵。在這種解讀下K?A →?A是普遍成立的：假設(shè)知道?A是經(jīng)典真，那么A為假，進(jìn)而A沒有構(gòu)造性證明。

最后考察對K(A ∨B)→(KA ∨KB)和KA →A的理解。

K(A∨B)→(KA∨KB)被解讀為：如果知道A∨B是經(jīng)典真，那么要么知道A是經(jīng)典真，要么知道B是經(jīng)典真。其中聯(lián)結(jié)K(A ∨B)和(KA ∨KB)的蘊(yùn)涵詞是經(jīng)典蘊(yùn)涵，聯(lián)結(jié)KA和KB的析取詞是經(jīng)典析取。在這種解讀下K(A ∨B)→(KA ∨KB)不是普遍成立的：參考KA被解讀為“知道A是直覺主義真或A是經(jīng)典真”的情況即可。

KA →A被解讀為：如果知道A是經(jīng)典真，那么A就是直覺主義真。其中聯(lián)結(jié)KA和A的蘊(yùn)涵詞是經(jīng)典蘊(yùn)涵。在這種解讀下KA →A不是普遍成立的：參考KA被解讀為“知道A是直覺主義真或A是經(jīng)典真”的情況即可。

5 結(jié)語

本文論證了IEL 的預(yù)期解釋與BHK 解釋的偏離在于缺失了對構(gòu)造性證明的要求，IEL 是對直覺主義命題邏輯的認(rèn)知擴(kuò)充，對于含有認(rèn)知算子K的公式來說，無法再從直觀上遵循直覺主義邏輯的BHK 解釋。相比而言，如果對直覺主義邏輯做一定限制（比如直覺主義相干邏輯），那么所得到的直覺主義邏輯的子系統(tǒng)自然遵循著直覺主義邏輯的BHK 解釋。對IEL 預(yù)期解釋的修正還能夠?yàn)镮EL 系統(tǒng)的對應(yīng)問題帶來啟示。首先，IPC 的內(nèi)定理刻畫了直覺主義真的命題邏輯規(guī)律；作為IPC 的擴(kuò)充系統(tǒng)，IEL 還刻畫了兼容直覺主義真和直覺主義知識的命題邏輯規(guī)律。再考慮中間邏輯12中間邏輯也被稱作超直覺主義邏輯（superintuitionistic logics）。（intermediate logics）系統(tǒng)，中間邏輯系統(tǒng)為數(shù)眾多，存在2?0（?0表示最小無窮基數(shù)）個(gè)中間邏輯（[4]，第59 頁），這些中間邏輯系統(tǒng)都是對直覺主義命題邏輯公理系統(tǒng)的擴(kuò)充，并且是經(jīng)典命題邏輯公理系統(tǒng)的子系統(tǒng)。最后，將上述兩種關(guān)系作類比可以提出猜測：IEL 系統(tǒng)對應(yīng)于某個(gè)中間邏輯系統(tǒng)。哥德爾（K.G?del）曾給出直覺主義命題邏輯系統(tǒng)IPC 和經(jīng)典模態(tài)邏輯系統(tǒng)S4 的對應(yīng)關(guān)系（[3]，第130 頁）：先根據(jù)一定規(guī)則（以遞歸定義的方式）把IPC的公式轉(zhuǎn)換為對應(yīng)的S4 的公式：

在此基礎(chǔ)上，A是IPC 系統(tǒng)的內(nèi)定理當(dāng)且僅當(dāng)At是S4 系統(tǒng)的內(nèi)定理。對這個(gè)結(jié)論做擴(kuò)展可以得到中間邏輯系統(tǒng)KC、LC 與S4 的擴(kuò)充系統(tǒng)S4.2、S4.3 的對應(yīng)如下（[3]，第136 頁）：

?A是KC 系統(tǒng)的內(nèi)定理當(dāng)且僅當(dāng)At是S4.2 系統(tǒng)的內(nèi)定理。

?A是LC 系統(tǒng)的內(nèi)定理當(dāng)且僅當(dāng)At是S4.3 系統(tǒng)的內(nèi)定理。

與之類似，上述猜測可以表述如下：

先根據(jù)一定的規(guī)則R把IPC 的公式轉(zhuǎn)換為對應(yīng)的IEL 的公式，令Γ 是某個(gè)中間邏輯系統(tǒng)，那么A是Γ 系統(tǒng)的內(nèi)定理當(dāng)且僅當(dāng)Att是IEL 的內(nèi)定理，其中Att是通過R從Γ 公式A轉(zhuǎn)換所得的IEL 公式。

上述猜測是否正確留給進(jìn)一步的研究。