杜文靜

(華東政法大學(xué)人文學(xué)院，上海200042)

一、引言

“循環(huán)并不可惡”［1］。Barwise和 Moss的著作《惡性循環(huán)——論非良基現(xiàn)象中的數(shù)學(xué)》建立了一套非良基集合理論，為各種循環(huán)現(xiàn)象(如，計算機(jī)科學(xué)中的流，公共知識中“知道”結(jié)構(gòu)的循環(huán)，哲學(xué)中的共通悖論、說謊者悖論、指稱悖論、高級游戲悖論以及羅素悖論等)提供了數(shù)學(xué)上的解釋［2］。Barwise和Moss的研究是建立在包含非良基集合的經(jīng)典集合論基礎(chǔ)之上的，即公理系統(tǒng)ZFA(ZFC-+AFA)。Rathjen斷言 Barwise和 Moss的大部分工作都可以建立在包含非良基集合的構(gòu)造性全域(constructive universe)的基礎(chǔ)上，而不是經(jīng)典集合全域。也就是說，Barwise和Moss的大部分工作都可以在構(gòu)造集合論(constructive set theory)的意義下進(jìn)行。正如公理系統(tǒng)ZFC對應(yīng)著康托經(jīng)典數(shù)學(xué)的形式化一樣，構(gòu)造集合論起源于Myhill的努力，他為了找到一個對應(yīng)Bishop的構(gòu)造性數(shù)學(xué)的形式化。后來，Aczel把Myhill的集合論完善成一個形式系統(tǒng)，并稱之為構(gòu)造集合論，記為CZF。在此背景下，第一概述構(gòu)造性數(shù)學(xué)的有關(guān)背景，并用實例展示它與傳統(tǒng)數(shù)學(xué)的區(qū)別，說明了構(gòu)造性數(shù)學(xué)的重要性;第二詳細(xì)闡述構(gòu)造集合論公理系統(tǒng)，說明它與其他公理系統(tǒng)的區(qū)別，為今后的研究工作——在構(gòu)造集合論意義下構(gòu)建非良基公理AFA的模型打下基礎(chǔ)。

二、構(gòu)造性數(shù)學(xué)

構(gòu)造性數(shù)學(xué)是現(xiàn)代數(shù)學(xué)研究的一個重要領(lǐng)域。在數(shù)學(xué)的討論中，常把能具體地給出某一對象或者能給出某一對象的計算方法者稱之為可構(gòu)造的。類似地，把能證實“存在一個對象x滿足性質(zhì) P”的證明稱為構(gòu)造的是指能從這個證明中具體地給出一個滿足性質(zhì)P的對象x;或者能從此證明中，得到一個機(jī)械的方法，使其經(jīng)有限步驟后，即能確定滿足性質(zhì)P的這個對象x。反之，也常把數(shù)學(xué)中的純存在性證明稱之為非構(gòu)造的。非構(gòu)造性的證明，是應(yīng)用反證法來證明，即通過證明如果否定一命題則將導(dǎo)致矛盾，從而肯定原命題。這種通過矛盾進(jìn)行證明是以亞里士多德邏輯的排中律為基礎(chǔ)的。這種方法在近代數(shù)學(xué)中是常見的。人們把堅持主張“要證明一個數(shù)學(xué)對象存在，必須指出這個對象是怎么構(gòu)造出來的”這種數(shù)學(xué)研究稱之為構(gòu)造性數(shù)學(xué)。構(gòu)造性數(shù)學(xué)的重要意義在于構(gòu)造性的研究不僅可以得出較為新穎、較為深刻的見解，而且構(gòu)造性的成果更便于應(yīng)用實際。

在非構(gòu)造性數(shù)學(xué)的研究中，往往主要考慮對象的一些性質(zhì)，如存在性、可能性等問題，不大關(guān)心如何求出解答、或?qū)⒛苄械姆椒ㄓ枰杂行У膶崿F(xiàn)。然而，應(yīng)用上對構(gòu)造性數(shù)學(xué)要求更為迫切，一個工程師對于方程解的存在性和唯一性不會有太多的注意，而更關(guān)心一些典型的特解，或利用微擾或迭代方法找出近似解［3］。構(gòu)造性數(shù)學(xué)要求遠(yuǎn)較非構(gòu)造性數(shù)學(xué)嚴(yán)格，因為它得把存在的對象具體找出來，所以，構(gòu)造性數(shù)學(xué)成立的每一定理對于非構(gòu)造性數(shù)學(xué)也成立，并且每個命題的構(gòu)造性證明絕對是這個命題的一個經(jīng)典證明，因此，在這個意義上，構(gòu)造性數(shù)學(xué)可以簡單地看成非構(gòu)造性數(shù)學(xué)的一個分支。事實上，早期以Borouwer為代表的直覺主義構(gòu)造性數(shù)學(xué)是為了解決數(shù)學(xué)的奠基問題，然而后期以Bishop、Myhill等所代表的新方向，他們的構(gòu)造性數(shù)學(xué)研究是在數(shù)學(xué)領(lǐng)域中，用普通邏輯于可編碼的對象和遞歸函數(shù)。他們所關(guān)心的，不是去解決數(shù)學(xué)奠基問題，而是要用構(gòu)造性方法來研究數(shù)學(xué)。他們把構(gòu)造性數(shù)學(xué)看成經(jīng)典數(shù)學(xué)的一個分支，在這個分支中所討論的對象(個體或映射)都要求是可計算的［4］。

構(gòu)造性數(shù)學(xué)不同于傳統(tǒng)的經(jīng)典數(shù)學(xué)，他的邏輯基礎(chǔ)是直覺主義邏輯。在構(gòu)造性數(shù)學(xué)中，數(shù)學(xué)家把“存在”嚴(yán)格解釋為“可以構(gòu)造”。為了進(jìn)行構(gòu)造性的工作，不僅需要把存在量詞，而且要把全稱量詞和所有邏輯連接詞都重新解釋為一些指令，利用這些指令去構(gòu)造關(guān)于邏輯表達(dá)式命題的證明。例如，在數(shù)學(xué)家們證明一個析取式P∨Q時，其中P和Q都是用形式或非形式語言表達(dá)的語法上正確的命題，就是要證明P或者證明Q。然而要構(gòu)造性地證明P∨Q，則要把P∨Q進(jìn)行自然的直覺主義解釋，即不僅要確定P和Q中至少有一個是正確的，而且要確定到底哪一個是正確的。在這種直覺主義解釋下，如果考慮一種特殊情形Q=?P，即Q是命題P的否定，數(shù)學(xué)家們將面臨一個嚴(yán)重的問題。要確定?P就是要去證明P蘊(yùn)含了一個矛盾(如0=1)。但是，在數(shù)學(xué)中，人們經(jīng)常會遇到既不能確定P也不能確定?P的情形，例如著名的哥德巴赫猜想:每個大于2的偶數(shù)都可以寫成兩個素數(shù)之和。盡管有很多大數(shù)學(xué)家對哥德巴赫猜想進(jìn)行過努力，但至今還是既不能證明它也不能否定它。由此可知，在構(gòu)造數(shù)學(xué)中，排中律并不普遍適用。這樣，經(jīng)典數(shù)學(xué)中的許多定理在構(gòu)造性數(shù)學(xué)中將難以得到證明。在經(jīng)典數(shù)學(xué)中，數(shù)學(xué)家把PVQ解釋成?(?P∧?Q)，也就說“與P和Q都是錯誤的矛盾”。這種解釋導(dǎo)致了存在量詞的理想主義解釋，即把?xP(x)解釋為?x?P(x)，也就是說“與對每個x來說P(x)都是錯誤的矛盾”。這些解釋都以亞里士多德邏輯的排中律(對每個命題P，要么P成立，要么?P成立)為基礎(chǔ)的。然而，這種解釋是需要付出代價的，因為在這種理想主義的解釋下產(chǎn)生的數(shù)學(xué)不能在計算模型(如遞歸函數(shù)論)中得到解釋。為了進(jìn)行構(gòu)造性的工作，必須回到剛才的自然直覺主義的解釋。在構(gòu)造性數(shù)學(xué)中，對邏輯聯(lián)接詞和量詞進(jìn)行如下的解釋:

∨:要證明 P∨Q，就必須要么有一個P的證明，要么有一個Q的證明;

∧:要證明P∧Q，就必須有一個P的證明，并且有一個Q的證明;

→:要證明P→Q，就必須找到一個算法，它可把P的一個證明轉(zhuǎn)化成Q的一個證明;

上面這些工作主要是由 Brouwer、Heyting、Kolmogorov等發(fā)起的，所以這些解釋被稱之為BHK解釋。為什么需要如此解釋邏輯呢?一方面是由于想給出數(shù)學(xué)的計算性解釋;另一方面是因為數(shù)學(xué)家想盡力用下面這種方式來發(fā)展數(shù)學(xué)，即如果一個定理斷言具有某個性質(zhì)P的對象x存在，那么這個定理的證明應(yīng)該包含一個算法，這個算法構(gòu)造出了這個對象x，并能證明它具有性質(zhì)P。下面，舉一個實例來說明構(gòu)造性方法與傳統(tǒng)非構(gòu)造性方法的區(qū)別。

例1.中國剩余定理:若整數(shù)m1，…，mr互素，整數(shù)u1，…，ur已知，則存在唯一的整數(shù) u∈［0，m1…mr］，使得

非構(gòu)造性證明:作映射

顯然，這個映射是單射，且兩邊都有M=m1…mr個元素，因而兩邊是一對一的，定理得證。這是個很漂亮的證明，但是卻不知道v具體是多少。

構(gòu)造性證明:取Ni=(m1…mj…mr)φ(mj)，其中 φ(mj)是歐拉函數(shù)，它等于(0，mj)中與mj互素的整數(shù)的個數(shù)，能夠算出來。于是

這樣，u1N1+u2N2+…urNr對M的余數(shù)就是要找的解。這個證明不但說明了解的存在，并且把這個解的具體值都求出來了，顯然可以從這個證明過程中提取一個程序，使之在計算機(jī)上可以實現(xiàn)。

從上面的例子可以看到，構(gòu)造性證明更直觀、更具體，能讓人切實感受到定理所描述的內(nèi)容，從中可以提取一個計算機(jī)程序使其機(jī)械化;而非構(gòu)造性證明卻有某種模糊性。

三、構(gòu)造集合論

Aczel利用 Martin Lof的類型論對CZF進(jìn)行了解釋，并證實了CZF的可構(gòu)造性。Aczel的這種解釋被認(rèn)為是典范的，并且可以看作是用類型論給CZF建立了一個標(biāo)準(zhǔn)模型。

構(gòu)造集合論為構(gòu)造性數(shù)學(xué)提供了一個標(biāo)準(zhǔn)的集合論框架，它是諸多構(gòu)造性數(shù)學(xué)集合論框架中的一種。構(gòu)造集合論之所以如此與眾不同是因為它使用的是經(jīng)典公理集合論的一階語言，并且沒有使用任何具體的構(gòu)造性思想。雖然CZF的邏輯是直覺邏輯，但其中不存在任何構(gòu)造性概念和構(gòu)造性對象。跟經(jīng)典集合一樣，這里只有集合這個概念。這就意味著構(gòu)造集合論中的數(shù)學(xué)與經(jīng)典集合論中的數(shù)學(xué)看起來非常相似。這樣的優(yōu)點在于如果遵守一些適當(dāng)?shù)脑瓌t，那么，通常數(shù)學(xué)的集合論表示的思想和慣例也能應(yīng)用到構(gòu)造性數(shù)學(xué)的集合論。而實際上，首先只需要遵守直覺邏輯中的邏輯推理原則，其次就是構(gòu)造集合論中的集合論公理。

構(gòu)造集合論CZF是經(jīng)典集合論ZF的一個變體，所使用的是直覺邏輯。ZF的另一個變體被稱之為直覺集合論IZF，IZF所使用的也是直覺邏輯。CZF與IZF的不同之處在于CZF避免了滿非直謂詞，而IZF沒有。CZF和IZF的語言跟經(jīng)典ZF系統(tǒng)一樣，它們也僅包含二元謂詞符號“∈”作為非邏輯符號。在直覺邏輯中，所有的二元聯(lián)接詞和量詞(∧，∨，→，?，?)都是原始定義的，即沒有一個是利用其他的聯(lián)接詞和量詞來定義的。跟通常一樣，可以利用蘊(yùn)含和常項“⊥”(假)來定義否定，即?φ是φ→⊥的縮寫。在此前提下，來定義公理系統(tǒng)CZF和IZF。CZF的邏輯是直覺謂詞邏輯，它與ZF公理系統(tǒng)的主要區(qū)別在以下幾方面:在CZF中，分離公理僅對△0-公式成立，這樣CZF有一個收集原則，而不是替換原則;在CZF中冪集公理被一個更弱子集收集原則所替代;另外，CZF使用集合的歸納原則，而不是基礎(chǔ)公理。系統(tǒng)IZF是CZF的推廣，它使用無限制的分離公理和冪集公理。

1978年，Aczel證明了如下結(jié)論:

CZF+EM=IZF+EM=ZF。

其中，EM表示排中律。這個結(jié)論說明了這三個公理系統(tǒng)之間的聯(lián)系。

近年來構(gòu)造性數(shù)學(xué)和構(gòu)造集合論的研究甚為引人注目，構(gòu)造性成果不斷涌現(xiàn)，這就說明在某些情況下用這種觀點來研究問題常常是大有裨益的。例如，數(shù)學(xué)家在構(gòu)造性證明中提取一個程序，使之可以用計算機(jī)實現(xiàn)，從而實現(xiàn)數(shù)學(xué)機(jī)械化的宏偉目標(biāo)。在許多情況下，構(gòu)造性的方法與存在性的方法常常是同樣地有效。構(gòu)造性的研究不僅可以得出較為新穎、較為深刻的見解，而且構(gòu)造性的成果更便于應(yīng)用。眾所周知，提供解答畢竟比純存在性地證明有解要有意義得多。當(dāng)一個數(shù)的存在能構(gòu)造地證明時，那么這個數(shù)不僅在理論上，而且實際上也可以計算出來。聯(lián)系到計算機(jī)科學(xué)已經(jīng)蓬勃發(fā)展，這種構(gòu)造性數(shù)學(xué)的研究更有其深遠(yuǎn)意義。

［1］張清宇.循環(huán)并不可惡——《Vicious Circles On the Mathematics of Non-Wellfounded Phenomena》評價［J］.哲學(xué)動態(tài)，2005，(4).

［2］J.Barwise，L.Moss.Vicious Circles:On the Mathematics of Non-Wellfounded Phenomena［M］.Stanford:CSLI，1996.

［3］吳文俊.復(fù)興構(gòu)造性的數(shù)學(xué)［J］.數(shù)學(xué)進(jìn)展，1985，(14).

［4］郝寧湘.構(gòu)造性數(shù)學(xué)及其哲學(xué)意義［J］.自然辯證法通訊，1997，(19).