程華清

1 直覺(jué)主義的構(gòu)造性思想

20 世紀(jì)初，對(duì)數(shù)學(xué)基礎(chǔ)的研究導(dǎo)致了直覺(jué)主義學(xué)派（intuitionistic school）的誕生，其代表人物是布勞威爾（L.E.J.Brouwer）。在布勞威爾看來(lái)，數(shù)學(xué)是一種心智的構(gòu)造性的活動(dòng)，數(shù)學(xué)定理表達(dá)的是純粹經(jīng)驗(yàn)的事實(shí)，數(shù)學(xué)不能建立在公理化方法基礎(chǔ)之上，直覺(jué)（直觀）就是數(shù)學(xué)可靠性的基礎(chǔ)。直覺(jué)主義學(xué)派的座右銘是“存在即被構(gòu)造”，這體現(xiàn)在它只接受心智可構(gòu)造的數(shù)學(xué)對(duì)象（對(duì)于所考慮的數(shù)學(xué)對(duì)象來(lái)說(shuō)，我們能夠通過(guò)一定的方法能行地得到它們）和心智可構(gòu)造的數(shù)學(xué)證明（對(duì)于一個(gè)數(shù)學(xué)命題所表達(dá)的內(nèi)容來(lái)說(shuō)，我們能夠通過(guò)一定的方法能行地驗(yàn)證它）。在心智可構(gòu)造的要求下，直覺(jué)主義學(xué)派拒斥實(shí)無(wú)窮而采納潛無(wú)窮觀。比如：在實(shí)無(wú)窮立場(chǎng)下，全體正整數(shù)能夠構(gòu)成一個(gè)作為獨(dú)立對(duì)象的集合，它是一個(gè)完成了的整體；而在心智可構(gòu)造的要求下，依賴于原始直覺(jué)，先構(gòu)建正整數(shù)1，再根據(jù)布勞威爾所提出的二一原則（two-oneness）（[1]，第85 頁(yè)），依次逐個(gè)地獲得后繼的正整數(shù)2,3,...，按照直覺(jué)主義的語(yǔ)言，這意味著“創(chuàng)造一個(gè)實(shí)體，接著再創(chuàng)造一個(gè)實(shí)體”，由此可構(gòu)造正整數(shù)的無(wú)窮序列1,2,3,...,n,...，但這種建構(gòu)過(guò)程是沒(méi)有終止的，因此，正整數(shù)的無(wú)窮序列不能作為一個(gè)完成了的整體來(lái)看待。

在布勞威爾對(duì)數(shù)學(xué)的獨(dú)特理解下，數(shù)學(xué)是不依賴于語(yǔ)言的。如果使用語(yǔ)言的話，那么語(yǔ)言就僅僅是記錄完成了的數(shù)學(xué)構(gòu)造的一種工具，通過(guò)語(yǔ)言這個(gè)媒介，不同個(gè)體可以交流他們所記錄的數(shù)學(xué)構(gòu)造。正如海廷（A.Heyting）所言：“直覺(jué)主義數(shù)學(xué)是一種心智的活動(dòng)，正因如此，每種語(yǔ)言（包括形式語(yǔ)言）都只是交流的工具。原則上說(shuō)，由于思想的可能性不能歸約為預(yù)先設(shè)置的有限規(guī)則，因此我們不可能創(chuàng)建一個(gè)由公式組成的形式系統(tǒng)使之等價(jià)于直覺(jué)主義數(shù)學(xué)。”（[3]，第311頁(yè)）邏輯作為在利用語(yǔ)言記錄完成了的數(shù)學(xué)構(gòu)造時(shí)所產(chǎn)生的形式規(guī)律，其有效性自然地依賴于數(shù)學(xué)的心智可構(gòu)造性，數(shù)學(xué)便成為了邏輯的基礎(chǔ)，而反之不然。

正是對(duì)數(shù)學(xué)的不同理解，使得直覺(jué)主義對(duì)“真”的理解有別于經(jīng)典意義上的“真”。在經(jīng)典意義上，對(duì)一個(gè)命題來(lái)說(shuō)，它是非真即假的，一個(gè)命題的真獨(dú)立于對(duì)它的證明；而在直覺(jué)主義看來(lái)，我們判定一個(gè)命題為真就必須要給出對(duì)它的構(gòu)造性證明，否則就不能判定這個(gè)命題為真。直覺(jué)主義對(duì)基本的邏輯聯(lián)結(jié)詞（否定?、合取∧、析取∨和蘊(yùn)涵→）以及全稱量詞?和存在量詞?的解釋也是基于構(gòu)造性立場(chǎng)的。接下來(lái)，我們遵循直覺(jué)主義構(gòu)造性思想，來(lái)構(gòu)建直覺(jué)主義邏輯的證明語(yǔ)義。由于構(gòu)造性證明是一種基于直觀理解的內(nèi)涵概念，這使得本文所構(gòu)建的直覺(jué)主義邏輯證明語(yǔ)義是一種內(nèi)涵語(yǔ)義。我們構(gòu)建證明語(yǔ)義的基本思路是：語(yǔ)義解釋從具體命題、具體的可構(gòu)造對(duì)象（個(gè)體）、具體的性質(zhì)和關(guān)系等出發(fā)，采用對(duì)公式A作解釋AI的方式，給出“直觀有效”的定義；避免使用集合概念，盡量貼近直觀。1在直覺(jué)主義邏輯中，對(duì)邏輯聯(lián)結(jié)詞、全稱量詞和存在量詞的標(biāo)準(zhǔn)語(yǔ)義解釋以布勞威爾、海廷和柯?tīng)柲缏宸颍ˋ.N.Kolmogorov）的工作為基礎(chǔ)，統(tǒng)稱為BHK 解釋。BHK 解釋說(shuō)明了：對(duì)于一個(gè)數(shù)學(xué)復(fù)合命題（包括全稱命題和存在命題）來(lái)說(shuō)，對(duì)它的具體構(gòu)造性證明通過(guò)以何種方式從它的直接子命題的具體構(gòu)造性證明而得到（參見(jiàn)[4]，第9 頁(yè)）。本文構(gòu)建的證明語(yǔ)義則是在對(duì)BHK 解釋弱化后的基礎(chǔ)上而建立的，體現(xiàn)在對(duì)否定詞、蘊(yùn)涵詞、全稱量詞和存在量詞的弱化解釋。

2 直覺(jué)主義命題邏輯的證明語(yǔ)義

定義2.1(原子命題和聯(lián)結(jié)詞的證明解釋).2參見(jiàn)[5]，第48–49 頁(yè)，本文做了補(bǔ)充和改動(dòng)。

1 對(duì)于一個(gè)原子命題φ來(lái)說(shuō)，判定φ為真當(dāng)且僅當(dāng)給出φ的構(gòu)造性證明。

2 對(duì)于一個(gè)否定命題?φ（意為“并非φ”）來(lái)說(shuō)，判定?φ為真當(dāng)且僅當(dāng)從任意假設(shè)的對(duì)φ的構(gòu)造性證明都將導(dǎo)致謬誤3謬誤作為初始概念，可以有多種表現(xiàn)形式，比如推出命題“B ∧?B”這樣的邏輯矛盾或推出如“0=1”這樣的荒謬句。（這意味著φ沒(méi)有構(gòu)造性證明），這時(shí)我們亦稱?φ獲得了構(gòu)造性證明。

3 對(duì)于一個(gè)合取命題φ ∧ψ（意為“φ并且ψ”）來(lái)說(shuō)，判定φ ∧ψ為真當(dāng)且僅當(dāng)同時(shí)給出對(duì)φ的構(gòu)造性證明和對(duì)ψ的構(gòu)造性證明，這時(shí)我們亦稱φ ∧ψ獲得了構(gòu)造性證明。

4 對(duì)于一個(gè)析取命題φ ∨ψ（意為“φ或者ψ”）來(lái)說(shuō)，判定φ ∨ψ為真當(dāng)且僅當(dāng)給出對(duì)φ的構(gòu)造性證明或給出對(duì)ψ的構(gòu)造性證明4另一種更強(qiáng)的對(duì)析取命題的證明解釋是：判定φ ∨ψ 為真當(dāng)且僅當(dāng)可指明φ、ψ 中的哪一個(gè)析取支是正確的，并且給出該析取支的構(gòu)造性證明。（參見(jiàn)[2]，第224 頁(yè)），這時(shí)我們亦稱φ ∨ψ獲得了構(gòu)造性證明。

5 對(duì)于一個(gè)蘊(yùn)涵命題φ →ψ（意為“如果φ，那么ψ”）來(lái)說(shuō)，判定φ →ψ為真當(dāng)且僅當(dāng)從任意假設(shè)的對(duì)φ的構(gòu)造性證明都能夠得到對(duì)ψ的構(gòu)造性證明，若φ是謬誤，不能獲得構(gòu)造性證明，亦判定φ →ψ為真。這時(shí)我們都稱φ →ψ獲得了構(gòu)造性證明。

依賴于上述證明解釋，我們可以進(jìn)一步構(gòu)建直覺(jué)主義命題邏輯的證明語(yǔ)義。下面，先給出直覺(jué)主義命題邏輯的形式語(yǔ)言L。

形式語(yǔ)言L由以下兩個(gè)部分構(gòu)成：

(1) 初始符號(hào)：

1 潛無(wú)窮個(gè)命題變?cè)簆1,p2,...。

2 否定聯(lián)結(jié)詞?、合取聯(lián)結(jié)詞∧、析取聯(lián)結(jié)詞∨和蘊(yùn)涵聯(lián)結(jié)詞→。

3 左右括號(hào)：(、)。

(2) 形成規(guī)則（A,B是任意公式）：

1 任意的命題變?cè)猵i是公式。

2 如果A是公式，那么?A是公式。

3 如果A,B是公式，那么(A ∧B),(A ∨B),(A →B)是公式。對(duì)一個(gè)公式A來(lái)說(shuō)，A自身，以及作為A的組成部分的那些公式都被稱為A的子公式。

定義2.2.L中的公式A的一個(gè)解釋（記為AI）由以下方式獲得：

1 將A中的每一個(gè)命題變?cè)冀忉尀橐粋€(gè)具體的（原子）命題，若A中含有不同的命題變?cè)?，那么不同的命題變?cè)梢越忉尀椴煌幕蛳嗤木唧w命題；

2 對(duì)聯(lián)結(jié)詞?、∧、∨和→作證明解釋（見(jiàn)定義2.12–5 ）。

對(duì)定義2.2 的說(shuō)明：1 公式A的一個(gè)解釋AI是一個(gè)確定的具體命題。2 若B是A的子公式并且AI是A的一個(gè)解釋，那么在AI的解釋下，B也獲得了相應(yīng)的解釋（記為BI），即某一個(gè)確定的具體命題。3 公式A的兩個(gè)解釋是否相同僅取決于對(duì)A中的每個(gè)命題變?cè)鞯慕忉屖欠裣嗤?/p>

定義2.3.稱一個(gè)L中的公式A是直觀有效的當(dāng)且僅當(dāng)對(duì)于A的任何解釋AI，AI都被判定為真，即總能給出對(duì)AI的構(gòu)造性證明。

定義2.1、定義2.2 和定義2.3 構(gòu)成了直覺(jué)主義命題邏輯的證明語(yǔ)義。以下給出直覺(jué)主義命題邏輯公理系統(tǒng)IP，它建立在形式語(yǔ)言L的基礎(chǔ)上，再加上以下兩部分構(gòu)成（[5]，第60–61 頁(yè)）：

(1)IP的公理（A,B,C是任意公式）：

公理IP1：(A →(B →A))

公理IP2：((A →(B →C))→((A →B)→(A →C)))

公理IP3：(A →(B →(A ∧B)))

公理IP4：((A ∧B)→A)

公理IP5：((A ∧B)→B)

公理IP6：(A →(A ∨B))

公理IP7：(B →(A ∨B))

公理IP8：((A →C)→((B →C)→((A ∨B)→C)))

公理IP9：((A →B)→((A →?B)→?A))

公理IP10：(?A →(A →B))

(2) 推理規(guī)則（A,B是任意公式）：

分離規(guī)則MP：由A和(A →B)可推出B。

若A是IP的公理，或者是由公理出發(fā)運(yùn)用MP規(guī)則推出的公式，則稱A是IP中的一個(gè)（內(nèi)）定理，記為?IP A。

下面的工作是證明直覺(jué)主義命題邏輯系統(tǒng)IP的可靠性，證明由以下引理和定理構(gòu)成。

引理2.1.系統(tǒng)IP的十條公理都是直觀有效的。

公理IP1.(A →(B →A))

證明.先給定對(duì)公理IP1的任意的一個(gè)解釋(A →(B →A))I。假設(shè)α是對(duì)AI的任意構(gòu)造性證明，那么對(duì)任意假設(shè)的對(duì)BI的構(gòu)造性證明β來(lái)說(shuō)，總能得到對(duì)AI的構(gòu)造性證明（即α），根據(jù)定義2.15 可知，(B →A)I獲得了構(gòu)造性證明，進(jìn)而獲得對(duì)(A →(B →A))I的構(gòu)造性證明。再根據(jù)定義2.3 可知，公理IP1是直觀有效的。

公理IP2.((A →(B →C))→((A →B)→(A →C)))

證明.先給定對(duì)公理IP2的任意的一個(gè)解釋((A →(B →C))→((A →B)→(A →C)))I。假設(shè)α是對(duì)(A →(B →C))I的任意構(gòu)造性證明、β是對(duì)(A →B)I的任意構(gòu)造性證明、γ是對(duì)AI的任意構(gòu)造性證明。根據(jù)定義2.15 可知，利用β，從γ能夠得到對(duì)BI的構(gòu)造性證明（記為γβ）；利用α，從γ能夠得到對(duì)(B →C)I的構(gòu)造性證明（記為γα）；利用γα，從γβ可以得到對(duì)CI的構(gòu)造性證明。于是(A →C)I獲得了構(gòu)造性證明，進(jìn)而((A →B)→(A →C))I和((A →(B →C))→((A →B)→(A →C)))I也獲得了構(gòu)造性證明。再根據(jù)定義2.3 可知，公理IP2是直觀有效的。

公理IP3.(A →(B →(A ∧B)))

證明.先給定對(duì)公理IP3的任意的一個(gè)解釋(A →(B →(A∧B)))I。假設(shè)α是對(duì)AI的任意構(gòu)造性證明，假設(shè)β是對(duì)BI的任意構(gòu)造性證明，根據(jù)定義2.13，(A∧B)I便獲得了構(gòu)造性證明。再根據(jù)定義2.15，(B →(A∧B))I和(A →(B →(A∧B)))I也獲得了構(gòu)造性證明。進(jìn)而根據(jù)定義2.3 可知，公理IP3是直觀有效的。

公理IP4.((A ∧B)→A)和公理IP5.((A ∧B)→B)

使用定義2.13、定義2.15 和定義2.3 即證，從略。

公理IP6.(A →(A ∨B))和公理IP7.(B →(A ∨B))

使用定義2.14、定義2.15 和定義2.3 即證，從略。

公理IP8.((A →C)→((B →C)→((A ∨B)→C)))

證明.先給定對(duì)公理IP8的任意的一個(gè)解釋((A →C)→((B →C)→((A∨B)→C)))I。假設(shè)α是對(duì)(A →C)I的任意構(gòu)造性證明、β是對(duì)(B →C)I的任意構(gòu)造性證明、γ是對(duì)(A ∨B)I的任意構(gòu)造性證明。根據(jù)定義2.14，或者給出對(duì)AI的構(gòu)造性證明（記為γA）或者給出對(duì)BI的構(gòu)造性證明（記為γB）。根據(jù)定義2.15，利用α，從γA能夠得到對(duì)CI的構(gòu)造性證明；利用β，從γB能夠得到對(duì)CI的構(gòu)造性證明。這樣，根據(jù)定義2.15 可知，先后可獲得((A ∨B)→C)I、((B →C)→((A ∨B)→C))I和((A →C)→((B →C)→((A ∨B)→C)))I的構(gòu)造性證明。再根據(jù)定義2.3 可知，公理IP8是直觀有效的。

公理IP9.(A →B)→((A →?B)→?A))

證明.先給定對(duì)公理IP9的任意的一個(gè)解釋((A →B)→((A →?B)→?A))I。假設(shè)α是對(duì)AI的任意構(gòu)造性證明、β是對(duì)(A →B)I的任意構(gòu)造性證明、γ是對(duì)(A →?B)I的任意構(gòu)造性證明。根據(jù)定義2.15，利用β，從α能夠得到對(duì)BI的構(gòu)造性證明（記為αβ）；利用γ，從α能夠得到對(duì)(?B)I的構(gòu)造性證明（記為αγ）。這樣就導(dǎo)致了謬誤。進(jìn)而根據(jù)定義2.12，(?A)I獲得了構(gòu)造性證明；由定義2.15，先后獲得了((A →?B)→?A)I和((A →B)→((A →?B)→?A))I的構(gòu)造性證明。再根據(jù)定義2.3 可知，公理IP9是直觀有效的。

公理IP10.(?A →(A →B))

證明.先給定對(duì)公理IP10的任意的一個(gè)解釋(?A →(A →B))I。假設(shè)α是對(duì)(?A)I的任意構(gòu)造性證明、β是對(duì)AI的任意構(gòu)造性證明。利用α，從β將得到謬誤，再根據(jù)定義2.15 可知，(A →B)I獲得了構(gòu)造性證明。進(jìn)而(?A →(A →B))I獲得了構(gòu)造性證明。再根據(jù)定義2.3 可知，公理IP10是直觀有效的。

引理2.2.A,B是任意的L的公式，如果A和(A →B)都是直觀有效的，那么B也是直觀有效的。

證明.設(shè)BI是公式B的任意給定的一個(gè)解釋，將BI擴(kuò)展為公式(A →B)的解釋(A →B)I，使得BI是(A →B)I解釋下獲得的相應(yīng)解釋，于是在(A →B)I解釋下可獲得公式A的解釋AI。已知A和(A →B)都是直觀有效的，由定義2.3 可知：AI和(A →B)I都被判定為真，再根據(jù)定義2.15 可知：BI被判定為真，所以B也是直觀有效的。

定理2.3(系統(tǒng)IP的可靠性定理).任給一L的公式A，如果?IP A，那么A是直觀有效的。

證明.根據(jù)引理2.1 和引理2.2，使用數(shù)學(xué)歸納法即證。

3 直覺(jué)主義謂詞邏輯的證明語(yǔ)義

先構(gòu)建直覺(jué)主義謂詞邏輯的形式語(yǔ)言L?。形式語(yǔ)言L?由以下兩部分構(gòu)成：

(1) 初始符號(hào)：

1 潛無(wú)窮個(gè)個(gè)體變?cè)簒1,x2,...。

2 個(gè)體常元：a1,a2,...。個(gè)體常元可以沒(méi)有，也可以是有窮個(gè)或潛無(wú)窮個(gè)，個(gè)體常元可以被解釋為特定的個(gè)體。

3 謂詞符號(hào)：A11,A12,...（一元謂詞符號(hào)）；A21,A22,...（二元謂詞符號(hào)）；...；An1,An2,...（n元謂詞符號(hào)）；...。謂詞符號(hào)至少有一個(gè)，可以是有窮個(gè)或潛無(wú)窮個(gè)，對(duì)于任意的正整數(shù)m,n來(lái)說(shuō)，Amn可以被解釋為第n個(gè)m元謂詞（一元謂詞可以被解釋為個(gè)體的性質(zhì)，m元謂詞（m ≥2）可以被解釋為m個(gè)個(gè)體之間的關(guān)系）。

4 否定聯(lián)結(jié)詞?、合取聯(lián)結(jié)詞∧、析取聯(lián)結(jié)詞∨、蘊(yùn)涵聯(lián)結(jié)詞→、全稱量詞?和存在量詞?。

5 左右括號(hào)：(、)。

個(gè)體變?cè)蛡€(gè)體常元被統(tǒng)稱為“項(xiàng)”。用t,t1,t2,...表示任意的項(xiàng)。

(2) 形成規(guī)則（A,B是任意公式）：

1 對(duì)于任意的m元謂詞符號(hào)Amn和任意的項(xiàng)t1,t2,...,tm，Amn(t1,t2,...,tm)是公式（被稱為原子公式）。

2 如果A是公式，那么?A是公式。

3 如果A,B是公式，那么(A ∧B),(A ∨B),(A →B)都是公式。

4 如果A是公式，那么?xiA和?xiA（i是任意正整數(shù)）都是公式。

接下來(lái)，我們給出一些關(guān)于L?的語(yǔ)型定義（[5]，第106–107 頁(yè)、第162 頁(yè)）：

1 對(duì)于任一公式A來(lái)說(shuō)，如果A中有子公式?xiB出現(xiàn)，那么稱B是這個(gè)?xi的轄域；如果A中有子公式?xiC出現(xiàn)，那么稱C是這個(gè)?xi的轄域。

2 對(duì)于任一有個(gè)體變?cè)霈F(xiàn)的公式A來(lái)說(shuō)，如果其中一個(gè)體變?cè)獂i（i是某個(gè)正整數(shù)）出現(xiàn)在?xi或?xi中，或者出現(xiàn)在?xi或?xi的轄域中，那么稱xi的這一次出現(xiàn)為約束的；否則，稱xi的這一次出現(xiàn)是自由的。如果xi在A中至少有一次自由出現(xiàn)，那么稱xi是A中的自由變?cè)Ｓ凶杂勺冊(cè)墓奖环Q為開(kāi)公式；沒(méi)有自由變?cè)墓奖环Q為閉公式。

對(duì)于公式A來(lái)說(shuō)，無(wú)論個(gè)體變?cè)獂i1,xi2,...,xin（i1,i2,...,in是n個(gè)正整數(shù)）是否在A中出現(xiàn)，都可以將A記為A(xi1,xi2,...,xin)。

3 對(duì)于公式A(xi)來(lái)說(shuō)，用A(t)表示：用項(xiàng)t替換A(xi)中xi的每一次自由出現(xiàn)而獲得的公式；如果xi不是A中的自由變?cè)敲碅(t)就是A(xi)。

4 若項(xiàng)t和個(gè)體變?cè)獂i滿足下列條件之一，就稱項(xiàng)t對(duì)于公式A中的xi是自由的：

1.xi在A中不出現(xiàn)或xi在A中僅有約束出現(xiàn)；

2.xi在A中有自由出現(xiàn)，并且項(xiàng)t是個(gè)體常元；

3.xi中有自由出現(xiàn)，項(xiàng)t是某一個(gè)體變?cè)獂j，并且每當(dāng)xi在A中自由出現(xiàn)時(shí)，xi都不在?xj或?xj的轄域內(nèi)。

以下，為了普遍性，我們把形式語(yǔ)言L?的初始符號(hào)中的個(gè)體常元和謂詞符號(hào)都選取為潛無(wú)窮個(gè)，在此基礎(chǔ)上，我們建立直覺(jué)主義謂詞邏輯的證明語(yǔ)義。5采用定義3.1 至定義3.5 以及引理3.1、引理3.2 的方式來(lái)構(gòu)建直覺(jué)主義謂詞邏輯證明語(yǔ)義的思想，是馮棉教授提出的。

定義3.1.L?中的公式A的一個(gè)解釋AI由以下七個(gè)部分構(gòu)成：

1 先確定一個(gè)論域（對(duì)象域），含有有限個(gè)對(duì)象（不能沒(méi)有對(duì)象）或潛無(wú)窮個(gè)對(duì)象。論域是個(gè)體變?cè)蛡€(gè)體常元的取值范圍。

2 將A中的每一個(gè)個(gè)體變?cè)冀忉尀檎撚蛑械娜我獾膶?duì)象。

3 對(duì)A中的每一個(gè)個(gè)體常元指定論域中的某一個(gè)對(duì)象（不同的個(gè)體常元可以指定論域中不同或相同的對(duì)象）。

4 將A中的每一個(gè)一元謂詞符號(hào)都解釋為論域中對(duì)象的某種性質(zhì)（不同的一元謂詞可以解釋為不同或相同的性質(zhì)）。

5 將A中每一個(gè)n(n ≥2)元謂詞符號(hào)都解釋為論域中n個(gè)對(duì)象之間的某種n元關(guān)系（不同的n元謂詞符號(hào)可以解釋為不同或相同的n元關(guān)系）。

6 聯(lián)結(jié)詞?意為“并非”、∧意為“并且”、∨意為“或者”、→意為“如果……，那么……”。

7?xi意為“對(duì)論域中的任意一個(gè)對(duì)象（都有……）”；?xi意為“論域中至少有一個(gè)對(duì)象（有……）”。

對(duì)定義3.1 的說(shuō)明：1 若A是一個(gè)閉公式，那么AI是一個(gè)具體命題；若A不是閉公式，那么AI不是一個(gè)具體的命題。2 若B是A的子公式，那么由AI可獲得B的相應(yīng)解釋BI。

定義3.2.A是L?的公式，AI是對(duì)A的一個(gè)解釋，A中共有m個(gè)（m ≥0）不同的自由個(gè)體變?cè)獂i1,xi2,...,xim，對(duì)它們分別指定AI論域中的對(duì)象c1,c2,...,cm（這些對(duì)象可以相同也可以不同），則稱其為“AI解釋下全部自由變?cè)囊粋€(gè)賦值”，記為AI(c1,c2,...,cm)。

對(duì)定義3.2 的說(shuō)明：AI(c1,c2,...,cm)是具體命題，若A中沒(méi)有自由變?cè)磎=0），那么AI(c1,c2,...,cm)就是AI。

定義3.3.A是L?的公式，AI是A的一個(gè)解釋，令φ′=AI(c1,c2,...,cm)（m ≥0）是“AI解釋下全部自由變?cè)囊粋€(gè)賦值”，它是一個(gè)具體命題，以下是“φ′被判定為真”的遞歸定義：

1 若A是原子公式，則φ′是原子命題，φ′被判定為真當(dāng)且僅當(dāng)給出φ′的構(gòu)造性證明。（形式同定義2.11 ）

2 若A是?B，則φ′是否定命題?φ，同定義2.12 。

3 若A是(B ∧C)，則φ′是合取命題φ ∧ψ，同定義2.13 。

4 若A是(B ∨C)，則φ′是析取命題φ ∨ψ，同定義2.14 。

5 若A是(B →C)，則φ′是蘊(yùn)涵命題φ →ψ，同定義2.15 。

6 若A是?xiB，則φ′是全稱命題?xiφ，有兩種情況：

(i)B中沒(méi)有xi的自由出現(xiàn)，則A與B有同樣的自由個(gè)體變?cè)?，這時(shí)φ=BI(c1,c2,...,cm)（它是“BI解釋下全部自由變?cè)囊粋€(gè)賦值”），則φ′被判定為真當(dāng)且僅當(dāng)φ被判定為真，這時(shí)亦稱φ′獲得了構(gòu)造性證明。

(ii)B中有xi的自由出現(xiàn)，則φ′被判定為真當(dāng)且僅當(dāng)對(duì)AI論域中的任何一個(gè)對(duì)象c，都可以找到BI(c1,c2,...,cm,c)（它是“BI解釋下全部自由變?cè)囊粋€(gè)賦值”，其中xi指定對(duì)象c）的構(gòu)造性證明，這時(shí)我們亦稱φ′獲得了構(gòu)造性證明。

7 若A是?xiB，則φ′是存在命題?xiφ，有兩種情況：

(i)B中沒(méi)有xi的自由出現(xiàn)，表述方式同6 (i)。

(ii)B中有xi的自由出現(xiàn)，則φ′被判定為真當(dāng)且僅當(dāng)能夠找到AI論域中的某一對(duì)象c，并給出BI(c1,c2,...,cm,c)（它是“BI解釋下全部自由變?cè)囊粋€(gè)賦值”，其中xi指定對(duì)象c）的構(gòu)造性證明，這時(shí)亦稱φ′獲得了構(gòu)造性證明。

定義3.4.A是L?的任意公式，AI是對(duì)A的一個(gè)解釋，則AI被判定為真當(dāng)且僅當(dāng)對(duì)于任意一個(gè)“AI解釋下全部自由變?cè)馁x值”AI(c1,c2,...,cm)（m ≥0），都可以獲得對(duì)AI(c1,c2,...,cm)的構(gòu)造性證明，這時(shí)我們亦稱AI獲得了構(gòu)造性證明。

由定義3.3 和定義3.4 立即獲得以下的引理3.1，它也可以視為“AI被判定為真”的遞歸定義：

引理3.1.A是L?的公式，AI是對(duì)A的一個(gè)解釋，則有：

1 如果A是原子公式Arn(t1,t2,...,tr)，則AI被判定為真當(dāng)且僅當(dāng)對(duì)于任意一個(gè)“AI解釋下全部自由變?cè)馁x值”AI(c1,c2,...,cm)（m ≤r），都可獲得對(duì)AI(c1,c2,...,cm)的構(gòu)造性證明。

2 如果A是公式?B，那么AI被判定為真當(dāng)且僅當(dāng)對(duì)于任意一個(gè)“AI解釋下全部自由變?cè)馁x值”AI(c1,c2,...,cm)=?BI(c1,c2,...,cm)，其中BI(c1,c2,...,cm)是“BI解釋下全部自由變?cè)馁x值”，從任意假設(shè)的對(duì)BI(c1,c2,...,cm)的構(gòu)造性證明都將導(dǎo)致謬誤。

3 如果A是公式(B∧C)，那么AI被判定為真當(dāng)且僅當(dāng)對(duì)于任意一個(gè)“AI解釋下全部自由變?cè)馁x值”AI(c1,c2,...,cm)=(BI(ci1,ci2,...,cik)∧CI(cj1,cj2,...,cjs))，其中BI(ci1,ci2,...,cik)是相應(yīng)的“BI解釋下全部自由變?cè)馁x值”，CI(cj1,cj2,...,cjs)是相應(yīng)的“CI解釋下全部自由變?cè)馁x值”，能同時(shí)給出對(duì)(BI(ci1,ci2,...,cik) 的構(gòu)造性證明和對(duì)CI(cj1,cj2,...,cjs) 的構(gòu)造性證明。

4 公式A是(B ∨C)，那么AI被判定為真當(dāng)且僅當(dāng)對(duì)于任意一個(gè)“AI解釋下全部自由變?cè)馁x值”AI(c1,c2,...,cm)=(BI(ci1,ci2,...,cik)∨CI(cj1,cj2,...,cjs))，其中BI(ci1,ci2,...,cik)是相應(yīng)的“BI解釋下全部自由變?cè)馁x值”，CI(cj1,cj2,...,cjs)是相應(yīng)的“CI解釋下全部自由變?cè)馁x值”，能給出對(duì)(BI(ci1,ci2,...,cik) 的構(gòu)造性證明或者給出對(duì)CI(cj1,cj2,...,cjs) 的構(gòu)造性證明。

5 如果A是公式(B →C)，那么AI被判定為真當(dāng)且僅當(dāng)對(duì)于任意一個(gè)“AI解釋下全部自由變?cè)馁x值”AI(c1,c2,...,cm)=(BI(ci1,ci2,...,cik)→CI(cj1,cj2,...,cjs))，其中BI(ci1,ci2,...,cik)是相應(yīng)的“BI解釋下全部自由變?cè)馁x值”，CI(cj1,cj2,...,cjs)是相應(yīng)的“CI解釋下全部自由變?cè)馁x值”，從任意假設(shè)的對(duì)BI(ci1,ci2,...,cik)的構(gòu)造性證明都能夠得到CI(cj1,cj2,...,cjs)的構(gòu)造性證明；如果任何BI(ci1,ci2,...,cik)都是謬誤，不能獲得構(gòu)造性證明，亦判定AI為真。

6 如果公式A是?xiB，有兩種情況：

(i)B中沒(méi)有xi的自由出現(xiàn)，則AI被判定為真當(dāng)且僅當(dāng)對(duì)于任意一個(gè)“AI解釋下全部自由變?cè)馁x值”AI(c1,c2,...,cm)，都可以獲得對(duì)BI(c1,c2,

...,cm)（它是“BI解釋下全部自由變?cè)囊粋€(gè)賦值”）的構(gòu)造性證明。

(ii)B中有xi的自由出現(xiàn)，則AI被判定為真當(dāng)且僅當(dāng)對(duì)于任意一個(gè)“AI解釋下全部自由變?cè)馁x值”AI(c1,c2,...,cm)，對(duì)AI論域中的任何一個(gè)對(duì)象c，都可以找到BI(c1,c2,...,cm,c)（它是“BI解釋下全部自由變?cè)囊粋€(gè)賦值”，其中xi指定對(duì)象c）的構(gòu)造性證明。

7 如果A是公式?xiB，有兩種情況：

(i)B中沒(méi)有xi的自由出現(xiàn)，表述方式同6 (i)。

(ii)B中有xi的自由出現(xiàn)，則AI被判定為真當(dāng)且僅當(dāng)對(duì)于任意一個(gè)“AI解釋下全部自由變?cè)馁x值”AI(c1,c2,...,cm)，都能夠找到AI論域中的某一對(duì)象c，并給出BI(c1,c2,...,cm,c)（它是“BI解釋下全部自由變?cè)囊粋€(gè)賦值”，其中xi指定對(duì)象c）的構(gòu)造性證明。

定義3.5.稱L?的一個(gè)公式A是直觀有效的當(dāng)且僅當(dāng)對(duì)A的任何解釋AI，AI都被判定為真，即總能給出對(duì)AI的構(gòu)造性證明。

由定義3.4 和定義3.5 立即獲得以下的引理3.2：

引理3.2.L?的一個(gè)公式A是直觀有效的當(dāng)且僅當(dāng)對(duì)A的任何解釋AI的任意一個(gè)“AI解釋下全部自由變?cè)馁x值”AI(c1,c2,...,cm)（m ≥0），都可以獲得對(duì)AI(c1,c2,...,cm)的構(gòu)造性證明。

定義3.1 至定義3.5 和引理3.1、引理3.2 構(gòu)成了直覺(jué)主義謂詞邏輯的證明語(yǔ)義，以下給出直覺(jué)主義謂詞邏輯公理系統(tǒng)IQ，它建立在形式語(yǔ)言L?的基礎(chǔ)上，再加上以下兩部分構(gòu)成：6[5]，第169–170 頁(yè)，表述有所改動(dòng)。

(1)IQ的公理：首先，把IP1到IP10中形式語(yǔ)言L 的任意公式A、B、C解釋成形式語(yǔ)言L?的任意公式，所得到的十條公理IQ1到IQ10即為IQ的前十條公理。除此之外，增加如下涉及量詞的公理（A,B是任意公式，i是任一正整數(shù)）：

公理IQ11：(?xi(A →B)→(?xiA →?xiB))

公理IQ12：(?xi(A →B)→(?xiA →?xiB))

公理IQ13：(A →?xiA)，其中個(gè)體變?cè)獂i在A中不自由出現(xiàn)

公理IQ14：(?xiA →A)，其中個(gè)體變?cè)獂i在A中不自由出現(xiàn)

公理IQ15：(?xiA(xi)→A(t))，其中項(xiàng)t對(duì)于A中的個(gè)體變?cè)獂i是自由的，A(t)是用t替換A(xi)中xi的每一次自由出現(xiàn)而獲得的公式。

公理IQ16：(A(t)→?xiA(xi))，其中項(xiàng)t對(duì)于A中的個(gè)體變?cè)獂i是自由的，A(t)是用t替換A(xi)中xi的每一次自由出現(xiàn)而獲得的公式。

(2) 推理規(guī)則（A,B是任意公式，i是任意正整數(shù)）：

分離規(guī)則MP：由A和(A →B)可推出B。

概括規(guī)則Gen：從A可推出?xiA。

若A是IQ的公理，或者是由公理出發(fā)運(yùn)用MP規(guī)則或Gen規(guī)則推出的公式，則稱A是IQ中的一個(gè)（內(nèi)）定理，記為?IQ An。

下面的工作是證明直覺(jué)主義謂詞邏輯系統(tǒng)IQ的可靠性，證明由以下引理和定理構(gòu)成。

引理3.3.系統(tǒng)IQ的16條公理都是直觀有效的。

首先，IQ1到IQ10的證明方法參照引理2.1，并使用定義3.3 至定義3.5 或引理3.1、引理3.2，從略，這里僅給出對(duì)IQ11到IQ16的證明。

公理IQ11.(?xi(A →B)→(?xiA →?xiB))

證明.給定對(duì)公理IQ11的任意的一個(gè)解釋(?xi(A →B)→(?xiA →?xiB))I，再給定任意一個(gè)“(?xi(A →B)→(?xiA →?xiB))I解釋下全部自由變?cè)馁x值”(?xi(A →B)→(?xiA →?xiB))I(c1,c2,...,cm)=(φ →(ψ →η))，其中φ=(?xi(A →B))I(c1,c2,...,cm)是相應(yīng)的“(?xi(A →B))I解釋下全部自由變?cè)馁x值”，ψ=((?xiA)I(ci1,ci2,...,cik)是相應(yīng)的“(?xiA)I解釋下全部自由變?cè)馁x值”，η=(?xiB)I(cj1,cj2,...,cjs))是相應(yīng)的“(?xiB)I解釋下全部自由變?cè)馁x值”。假設(shè)α和β分別是φ和ψ的構(gòu)造性證明，以下證η可獲得構(gòu)造性證明。分兩種情況討論：

(1) (A →B)中沒(méi)有xi的自由出現(xiàn)（這時(shí)A和B中也沒(méi)有xi的自由出現(xiàn)），根據(jù)定義3.36 (i)，利用α和β能夠分別得到θ=(A →B)I(c1,c2,...,cm)（它是“(A →B)I解釋下全部自由變?cè)囊粋€(gè)賦值”）和δ=AI(ci1,ci2,...,cik)（它是“AI解釋下全部自由變?cè)囊粋€(gè)賦值”）的構(gòu)造性證明，而θ=(δ →λ)，其中λ=BI(cj1,cj2,...,cjs)（它是“BI解釋下全部自由變?cè)囊粋€(gè)賦值”），再根據(jù)定義3.35，能夠獲得λ的構(gòu)造性證明，進(jìn)而根據(jù)定義3.36 (i)，η獲得了構(gòu)造性證明。

(2) (A →B)中有xi的自由出現(xiàn)，根據(jù)定義3.36 (ii)，對(duì)論域中的任一對(duì)象c，利用α能夠得到θ=(A →B)I(c1,c2,...,cm,c)（它是“(A →B)I解釋下全部自由變?cè)囊粋€(gè)賦值”，其中xi指定對(duì)象c）的構(gòu)造性證明，又有兩種可能性：

(i) 當(dāng)A中有xi的自由出現(xiàn)時(shí)，利用β能夠得到δ=AI(ci1,ci2,...,cik,c)（它是“AI解釋下全部自由變?cè)囊粋€(gè)賦值”，其中xi指定對(duì)象c）的構(gòu)造性證明，而θ=(δ →λ)，其中λ=BI(cj1,cj2,...,cjs)（若B中沒(méi)有xi的自由出現(xiàn)）或λ=BI(cj1,cj2,...,cjs,c)（它是“BI解釋下全部自由變?cè)囊粋€(gè)賦值”，其中xi指定對(duì)象c，而B(niǎo)中有xi的自由出現(xiàn)），再根據(jù)定義3.35，能夠獲得λ的構(gòu)造性證明，進(jìn)而根據(jù)定義3.36，η獲得了構(gòu)造性證明。

(ii) 當(dāng)A中沒(méi)有xi的自由出現(xiàn)時(shí)，利用β能夠得到δ=AI(ci1,ci2,...,cik)的構(gòu)造性證明，而θ=(δ →λ)，其中λ=BI(cj1,cj2,...,cjs,c)，再根據(jù)定義3.35，能夠獲得λ的構(gòu)造性證明，進(jìn)而根據(jù)定義3.36 (ii)，η獲得了構(gòu)造性證明。

最后，利用α和β，從(1)(2)出發(fā)，根據(jù)定義3.35 可知(φ →(ψ →η))獲得了構(gòu)造性證明，再由引理3.2 推知公理IQ11是直觀有效的。

公理IQ12.(?xi(A →B)→(?xiA →?xiB))

參照公理IQ11的證明方法，并使用定義3.35、定義3.37 和引理3.2，從略。

公理IQ13.(A →?xiA)，其中個(gè)體變?cè)獂i在A中不自由出現(xiàn)。

證明.給定對(duì)公理IQ13任意的一個(gè)解釋(A →?xiA)I，再給定任意一個(gè)“(A →?xiA)I解釋下全部自由變?cè)馁x值”(A →?xiA)I(c1,c2,...,cm)=(φ →ψ)，其中φ=AI(c1,c2,...,cm) 是相應(yīng)的“AI解釋下全部自由變?cè)馁x值”，ψ=(?xiA)I(c1,c2,...,cm)是相應(yīng)的“(?xiA)I解釋下全部自由變?cè)馁x值”。假設(shè)α是φ的任意構(gòu)造性證明，根據(jù)定義3.36 (i)，ψ獲得了構(gòu)造性證明，再根據(jù)定義3.3 5，(φ →ψ)獲得了構(gòu)造性證明，進(jìn)而根據(jù)引理3.2，公理IQ13是直觀有效的。

公理IQ14.(?xiA →A)，其中個(gè)體變?cè)獂i在A中不自由出現(xiàn)。

參照公理IQ13的證明方法，并使用定義3.35、定義3.37 (i) 和引理3.2，從略。

公理IQ15.(?xiA(xi)→A(t))，其中項(xiàng)t對(duì)于A中的個(gè)體變?cè)獂i是自由的。

證明.給定對(duì)公理IQ15任意的一個(gè)解釋(?xiA(xi)→A(t))I，再給定任意一個(gè)“(?xiA(xi)→A(t))I解釋下全部自由變?cè)馁x值”(?xiA(xi)→A(t))I(c1,c2,...,cm)=(φ →ψ)。假設(shè)α是φ的構(gòu)造性證明，以下證ψ可獲得構(gòu)造性證明，分三種情況討論：

(1)xi不在A中自由出現(xiàn)，A(t)是A(xi)（即A）。這時(shí)φ=(?xiA)I(c1,c2,...,cm)是相應(yīng)的“(?xiA(xi))I解釋下全部自由變?cè)馁x值”，ψ=AI(c1,c2,...,cm)是相應(yīng)的“A(t)I解釋下全部自由變?cè)馁x值”。從α出發(fā)，根據(jù)定義3.36(i)，ψ獲得了構(gòu)造性證明。

(2)xi在A中有自由出現(xiàn)并且t是某一個(gè)體常元as，A(t)是A(as)。這時(shí)φ=(?xiA(xi))I(c1,c2,...,cm),ψ=(A(as))I(c1,c2,...,cm)，設(shè)(?xiA(xi)→A(t))I解釋下對(duì)as指定的論域中的對(duì)象是c，根據(jù)定義3.36 (ii)，通過(guò)α能夠得到(A(xi))I(c1,c2,...,cm,c)（它是“(A(xi))I解釋下全部自由變?cè)囊粋€(gè)賦值”，其中xi指定對(duì)象c）的構(gòu)造性證明，而(A(xi))I(c1,c2,...,cm,c)=ψ，于是ψ獲得了構(gòu)造性證明。

(3)xi在A中有自由出現(xiàn)，t是某一個(gè)體變?cè)獂j，并且每當(dāng)xi在A中自由出現(xiàn)時(shí)，xi都不在?xj或?xj的轄域內(nèi)，A(t)是A(xj)。設(shè)(?xiA(xi)→A(t))I解釋下對(duì)xj指定的論域中的對(duì)象是ci（它是c1,c2,...,cm中的某一個(gè)對(duì)象），這時(shí)φ=(?xiA(xi))I(c1,c2,...,ci?1,ci+1,...,cm)（若?xiA(xi)中沒(méi)有xj的自由出現(xiàn)）或φ=(?xiA(xi))I(c1,c2,...,cm)（其中xj指定對(duì)象ci，而?xiA(xi)中有xj的自由出現(xiàn)），ψ=(A(xj))I(c1,c2,...,cm)（它是“(A(xj))I解釋下全部自由變?cè)馁x值”，其中xj指定對(duì)象ci），根據(jù)定義3.36 (ii)，通過(guò)α能夠得到(A(xi))I(c1,c2,...,cm)（它是“(A(xi))I解釋下全部自由變?cè)囊粋€(gè)賦值”，其中xi指定對(duì)象ci）的構(gòu)造性證明，而(A(xi))I(c1,c2,...,cm)=ψ，于是ψ獲得了構(gòu)造性證明。

最后，利用α,從(1)(2)(3)出發(fā)，根據(jù)定義3.35 可知(φ →ψ)獲得了構(gòu)造性證明，再由引理3.2 推知公理IQ15是直觀有效的。

公理IQ16.(A(t)→?xiA(xi))，其中項(xiàng)t對(duì)于A中的個(gè)體變?cè)獂i是自由的。

參照公理IQ15的證明方法，并使用定義3.35、定義3.37 和引理3.2，從略。

引理3.4.A，B是任意的L?的公式，如果A和(A →B)都是直觀有效的，那么B也是直觀有效的。

證明方法參照引理2.2，并使用定義3.3 至定義3.5 或引理3.1、引理3.2，從略。

引理3.5.A是L?中任意公式，若A是直觀有效的，則?xiA也是直觀有效的。

證明.給定?xiA的任意一個(gè)解釋(?xiA)I，再給定任意一個(gè)“(?xiA)I解釋下全部自由變?cè)馁x值”(?xiA)I(c1,c2,...,cm)=φ。分兩種情況討論：

(1) 當(dāng)xi在A中沒(méi)有自由出現(xiàn)時(shí)，ψ=AI(c1,c2,...,cm)是相應(yīng)的“AI解釋下全部自由變?cè)馁x值”，已知A是直觀有效的，由引理3.2 知ψ可獲得構(gòu)造性證明，再由定義3.36 (i)，φ可獲得構(gòu)造性證明，進(jìn)而由引理3.2 知?xiA是直觀有效的。

(2) 當(dāng)xi是A中的自由變?cè)獣r(shí)，設(shè)c是AI論域中的任意一個(gè)對(duì)象，已知A是直觀有效的，由引理3.2 知AI(c1,c2,...,cm,c)（它是“AI解釋下全部自由變?cè)囊粋€(gè)賦值”，其中xi指定對(duì)象c）都能夠獲得構(gòu)造性證明，再根據(jù)引理3.16 (ii)，φ可獲得構(gòu)造性證明，進(jìn)而根據(jù)引理3.2 知?xiA是直觀有效的。

定理3.6(系統(tǒng)IQ的可靠性定理).任給一L?的A，如果?IQ A，那么A是直觀有效的。

證明.根據(jù)引理3.3、引理3.4 和引理3.5，使用數(shù)學(xué)歸納法即證。