直觀主義

在數學哲學和邏輯中，直覺主義（英語：Intuitionism），或者新直覺主義（Neointuitionism ）（對應於前直覺主義（Preintuitionism）），是用人類的構造性思維活動進行數學研究的方法。也可翻譯成直觀主義。 ^[1] 

任何數學對象被視為思維構造的產物，所以一個對象的存在性等價於它的構造的可能性。這和古典的方法不同，因為根據古典方法，一個實體的存在可以通過否定它的不存在來證明。對直覺主義者來説，這是不正確的：不存在的否定不表示可能找到存在的構造證明。正因為如此，直覺主義是數學結構主義的一種；但它不是唯一的一類。

直覺主義把數學命題的正確性和它可以被證明等同起來；如果數學對象純粹是精神上的構造，還有什麼其它法則可以用作真實性的檢驗呢（如同直覺主義者所説的一樣）？這意味着直覺主義者對一個數學命題的含義，可能與古典的數學家有不同理解。例如，説A或B，對於一個直覺主義者，是宣稱A或是B可以被“證明”，而非兩者之一“為真”。值得一提的是，只允許A或非A的排中律，在直覺主義邏輯中是不被允許的；因為不能假設人們總是能夠證明命題A或它的否定命題。

直覺主義也拒絕承認實無窮的抽象概念；也就是説，它不把像所有自然數的集合或任意有理數的序列這樣的無窮當作實體來考慮。這要求將集合論和微積分的基礎分別重新構造為構造主義集合論和構造主義分析。

在元理論中，一種認識論認為通過一種直觀的推理可以馬上知道關於道德的敍述是否正確。在17和18世紀，卡德沃斯和莫爾（1614~1687），克拉克（1675~1729）和普萊斯（1723~1729）是直觀主義的維護者；在20世紀，其支持者包括普理查德（1871~1947）、穆爾和羅斯。那些可以直接理解的道德真理有各種類別，對應的直觀主義也就不同。例如，穆爾認為某些事情具有道德價值這一點就是毋庸置疑的正確的，而羅斯則認為我們立即能知道的就是我們有責任去做這類事情。 ^[2] 

由於悖論的出現，產生了數學基礎論的危機，其後30年間，圍繞着各種問題進行熱烈的爭論，出現相互對立的邏輯主義、直覺主義、形式主義三大學派。從1900年到1930年左右，數學的危機使許多數學家都捲入到一場大辯論當中。他們看到這次危機涉及數學的根本，必須對數學的哲學基礎加以嚴密的考察。在這場大辯論中，原來的不明顯的意見分歧擴展成為學派的爭論，以羅素為代表的邏輯主義，以布勞威爾為代表的直覺主義，以希爾伯特為代表的形式主義三大學派應運而生。

1930年，哥德爾不完全性定理的證明暴露了各派的弱點，哲學的爭論冷淡了下去。此後各派力量沿着自己的道路發展演化。特別是羅素等人企圖從邏輯中推出全部數學。推導過程極為繁瑣，以至花上幾百頁才能把數1定義出來，無怪乎法國大數學家彭加勒挖苦他們説：“這是一個可欽佩的定義，它獻給從來沒有聽説過1的人。”從哲學上來講，也很難在這個體系中補充直觀和經驗的概念，從而使數學成為“不結果實的”、純粹形式的演繹科學。不過，羅素等人以符號形式實現邏輯數學化，從而極大地推動數理邏輯的發展，這種功績是不可抹殺的。

直覺主義者走向另一個極端，他們否定實在的無限。克羅內克甚至否定無理數的存在，連圓周率π都認為不存在，因為從整數出發，無法造出π來。代表人物是布勞威爾。他在1907年發表《論數學基礎》，正式建立起直覺主義數學。他們否定排中律，也就是認為存在着既不能證明也不能否證的命題。他們堅持所有定義和命題都必須通過構造來實現，從而根本不承認無窮集合論。雖然他們因此消除了悖論，但是也因此否定了大部分經典數學。他們把數學建立在構造的基礎上，儘管他們取得相當的成就，但也無法與整個數學的大洋相提並論。反對直覺主義最有力的是希爾伯特。

希爾伯特他第一篇證明論的工作是1922年發表的，在《數學的新基礎：第一篇》中，他論述如何把數論用有限方法討論，而數學本身卻一般須用超窮方法。他指出用符號邏輯方法可以把命題和證明加以形式化，而把這些形式化的公式及證明直接當做研究對象。在1922年在德國自然科學家協會萊比錫會議上，他做了《數學的邏輯基礎》的演講，更進一步提出了證明方法。要求有限主義，即經過有限步不推出矛盾來即為證明可靠，這稱為希爾伯特計劃。其實早先弗雷格已經堅持認為需要有明顯的符號系統，明顯的公理及推演規則，明顯的證明。

希爾伯特定走的更遠，他提出這樣一種明顯理論本身也做為一種數學研究的對象，且應用適當的方法來判定它是否無矛盾，這種做法一般稱為元數學。希爾伯特建議兩條最基本的原則：一、形式主義原則：所有符號完全看做沒有意義的內容，即使將符號、公式或證明的任何有意的意義或可能的解釋也不管，而只是把它們看作純粹的形式對象，研究它們的結構性質；二、有限主義原則，即總能在有限機械步驟之內驗證形式理論之內一串公式是否一個證明。應用數學方法於這樣一個形式理論，避免涉及無窮的推斷，這就排除了康托爾**論的方法。這個思想是隻應用靠得住的方法，因為要證明數學或其一部分無矛盾的方法是大家公認可靠的，整個數學才有牢固的基礎。希爾伯特認為數學的真理所在就是沒有矛盾，而不在於能否構造出來。他提出的形式主義的主要論點是：數學本身是形式系統的集合，每個形式系統都包含自己的邏輯、概念、公理及推理規則；數學的任務就是發展出每一個這樣的演繹系統，在每一個系統中，定理的證明通過一系列程序得到，只要這種推演過程不產生矛盾出來。為此，希爾伯特以數學的證明為研究對象，提出所謂希爾伯特綱領，成為後來證明論（元數學）的來源。在希爾伯特綱領中，希爾伯特要求無矛盾性的證明通過有限的構造步驟達到，而且力圖首先在初等算術的系統中實現。但是1931年奧地利數學家哥德爾證明這個要求是達不到的。

直覺主義邏輯或構造性邏輯是最初由阿蘭德·海廷開發的為魯伊茲·布勞威爾的數學直覺主義計劃提供形式基礎的符號邏輯。這個系統保持跨越生成導出命題的變換的證實性而不是真理性。從實用的觀點，也有使用直覺邏輯的強烈動機，因為它有存在性質，這使它還適合其他形式的數學構造主義。

直覺類型論、或構造類型論、或Martin-Löf 類型論、或就叫類型論是基於數學構造主義的函數式編程語言、邏輯和集合論。直覺類型論由瑞典數學家和哲學家Per Martin-Löf在1972年介入。 Martin-Löf 已經多次修改了它的提議；先是非直謂性的而後是直謂性的，先是外延的而後是內涵的類型論變體。

直覺類型論基於的是命題和類型的同一: 一個命題同一於它的證明的類型。這種同一通常叫做Curry-Howard同構，它最初公式化了命題邏輯和簡單類型 lambda 演算。類型論通過介入包含着值的依賴類型把這種同一擴展到謂詞邏輯。類型論內在化了Brouwer、Heyting和Kolmogorov提議的叫做BHK釋義的直覺邏輯釋義。類型論的類型扮演了類似於集合在集合論的角色，但是在類型論中的函數總是可計算的。