思考機器（一）——計算機是怎樣進行邏輯思考的

 

上個世紀九十年代，人工智能曾是計算機研究領域的熱門。當時AI發展的重點在於用形式系統模擬人腦的邏輯思維，即如何用符號表示推理法則，再令機器像人腦一樣運用規則進行推演與判斷。這類AI在短暫的喧囂后歸於沉寂，除了在數學考場上，多數情況下人腦對事物的判斷，是源於大量經驗累積中涌現的直覺，而非嚴密的邏輯推理。

 

到了新世紀，人工智能再度成為熱門話題，如今的AI幾乎已經是神經網絡的同義詞。也許無論是硅基還是碳基系統，真正的智力在於學習新知識的能力，而非對於知識的表達與運用。相比今天的人工智能，傳統的形式系統只應用於某些特定領域，如計算機輔助證明，程序的形式化驗證等等。然而，這不表示形式化已經是過時的知識。理解形式系統的思想，尤其是與之密切相關的類型系統，不僅有助於正確的程序語言表達，更能理解代碼的本質。本文簡單討論一下形式化驗證的基石——柯里-霍華德同構，以此來說明計算機為什么可以進行邏輯推理，以及計算機是怎樣進行邏輯推理的。

 

一、什么是邏輯？什么是形式？

 

三段論奠定直覺邏輯

——“蘇格拉底是人，人會死，所以蘇格拉底會死”

 

討論為什么之前，先說是什么。最古老的邏輯可以追溯到三段論，即所謂直覺邏輯。在蘇格拉底這個例子中，每一句陳述由一個主語（蘇格拉底，人）和一個謂詞（是人，會死）組成。其中“人”、“死”可以看作所陳述的主語的特性。

 

主語與特性之間用什么系詞來表達，不影響對陳述的理解。在自然語言中，我們可能說蘇格拉底是人；蘇格拉底系人；蘇格拉底者，人也。這種依靠自然語言的表達並不嚴謹，以致完全不同的陳述可能表達同一意義，反之同一陳述也可能有不同的理解。因此，邏輯學家們選擇使用統一的抽象符號，並賦予其嚴格的含義與推導規則，例如，四則運算的符號與法則就是放諸四海而皆准的。在蘇格拉底這個例子中，我們可以用➞來表達“是”、“會”這一表示屬性的詞匯，用⇒表示“所以”，“導出”這類蘊涵着推理關系的詞匯：

 

((蘇格拉底➞人) and (人➞死))⇒(蘇格拉底➞死)

 

在直覺邏輯的世界中，這是一個特定的表達式。在這個特例里，如果我們將所陳述的對象蘇格拉底完全替換為柏拉圖，並不影響表示式的正確性。如果我們用符號S代替蘇格拉底，用符號H代替人，用符號D代替死，將and簡化為符號×，以上的將例子進一步抽象為

 

((S➞H)×(H➞D))⇒(S➞D)

 

此處的S/H/D不再是具體的事物或特性，而是一個變量。將該變量替換為任何人事，在邏輯上都是成立的。比如令S=蘋果，H=水果，D=好吃，可以得出陳述

 

((蘋果➞水果)×(水果➞好吃))⇒(蘋果➞好吃)

 

因此，((S➞H)×(H➞D))⇒(S➞D)不再是一個具體的陳述，而是一條抽象的推理法則。蘇格拉底則是這條法則的一次應用。

 

如果我們給一個三段論運算器編入這一法則，再提供形如(S➞H)和(H➞D)兩個陳述，它總是可以得出形如(S➞D)這一結論。通過定義嚴格的語法與推理規則，構建起一個推演系統的過程，稱作形式化，該系統即形式系統。

 

舉例來說，數學就是一種形式系統。在自然語言中，我們可能將一個計算描述為二十乘以三十，三十個二十，twenty times thirty等等。但是使用數學語言時，全世界小學及以上文憑的人都會將這個計算過程表述為 20×30=600

 

形式與意義是相對獨立的

——玄之又玄，眾妙之門

 

在形式系統中，重要的是推理規則，而不是名字和符號。在上述蘇格拉底的例子，將同一個表達式中的事物名換為其他符號，完全不影響推理的過程。

 

舉例來說，(S➞D)既可以用作人類學表述，即蘇格拉底會死；也可以用作飲食文化陳述，即蘋果好吃。我們只需要將S和D等量替換為不同的敘述對象就行了。甚至在某個星球上，“蘇格拉底”指一種紅紅的，圓圓的水果，“人”指一類多汁的植物果實，而“死”的自然語言中的意思是“美味”。那么當外星人說出

((蘇格拉底➞人)×(人➞死))⇒(蘇格拉底➞死)

這個陳述時，實際上是在表達他們對食堂供餐的意見。

 

可以說，形式系統只關心“名（name）”的同一性，即在一次完整的推理中，同一個名字指向的實際意義是相同的。名字的實際意義究竟就是什么，則是由人為賦予的。人們會將形式系統中的變量或常量名映射為他們心中的某種概念。形式系統中的表達式是抽象的，人們對表達式的解釋則是具象的。同一個抽象的陳述，可能映射為不同的物理解釋；當然，同一個物理意義也以用不同的名字來表示。

 

例如，在上文提到的三段論運算器中，我們只要提供形如(S➞H)和(H➞D)的陳述，它總是能得出形如(S➞D)的結論。如果我們將其中的符號➞換成⊂，那么只要給這台機器提供(S⊂H)和(H⊂D)，它總能得出結論(S⊂D)，雖然我們依然可以宣稱此處⊂符號的含義是直覺邏輯中用於表示S特性D的符號，這個運算器是一個三段論運算器，但是顯然，對於

 

((S⊂H)×(H⊂D))⇒(S⊂D)

 

更直覺的解釋是集合論中的一條運算法則，其中“⊂”是集合論中表示子集關系的符號。

 

除了符號不同，這台機器的運算法則沒有任何變化，但是將➞替換為⊂之后，人們直觀上會將它當作一台集合論計算器，而不再是三段論計算器。 這種符號與意義之間的映射是人為賦予的，把⊂當作集合論計算符號，只是人類長期以來的經驗習慣而已。在這個例子里，一套形式系統可以同時映射為兩種不同的實際運算，⊂既可以表示三段論，也可以表示集合論；反之，兩套不同的符號系統➞和⊂，都可以表示三段論運算。用一句古老的箴言來說，道【可道】，非【常道】；名【可名】，非【常名】。

 

以計算機的基本構成元件——邏輯門為例。一個異或門的輸入真值表是

（0，0）➞0

（1，0）➞1

（0，1）➞1

（1，1）➞0

此處1表示布爾運算中的true，0表示false。但是如果把0解釋為二進制中的0，1代表二進制中的1，我們會發現這套運算法則恰好與二進制加法的個位運算是一致的。因此，同一個元件既可以表示異或運算，也可以表示加法運算，這取決於我們如何解釋符號1與0的含義。加法器就是由這樣的門電路組成的。

 

再以數學這一形式系統為例，假設在平行世界的數學中，用#表示加法，用？表示等於，他們會有這樣一條加法法則

5?3#2

即我們世界中的

5=3+2

但是在另一個平行世界中，他們把#解釋為等於，把?解釋為減去，那么這條法則變成了

5-3=2

這其實是一條減法法則。

這個例子可以說明，所有形如a=b+c的加法表達式和形如a-b=c的減法表達式在形式上是一致的。我們完全可以把a=b+c中的+理解為等於，=理解為減去，所有的運算依然是成立的。

 

只要兩種運算基本法則的形式完全相同，就可以用同一套形式系統來表示，使用這套系統推演出的一切表達式都可以有兩種解釋。在這種情況下，我們說這兩種運算是同構的。

 

二、什么樣的形式能表示邏輯？

形式化的直覺邏輯

——我是阿爾法，我是歐米伽

 

下面我們來討論一種簡單的邏輯系統——直覺邏輯。直覺邏輯有許多不同的表示方式，這里我們采用希爾伯特風格的形式系統。這一系統有兩條公理形式，即所有形如

α→β→α （1）

(α→β→γ)→(α→β)→α→γ （2）

 

都是公理。其中每個字母代表一個不可分的元命題，或者一個表達式。該系統唯一的推演規則是，如果α→β和α是定理，那么β也是定理

 

注意此處的定理沒有非真即假的概念，證明一個表達式是定理的唯一方式是用公理和推演規則推出它，推出它的否命題為假是無效的，也就是說，這個系統不能使用反證法

 

希爾伯特表達式是右結合的，也就是在表達式的右半部分加括號不影響其含義。公式（1）可以寫作

α→(β→α)

也就是說如果α是定理，那么β→α也是定理。公式（2）則可以寫作

(α→(β→γ))→((α→β)→(α→γ))

用自然語言來說，如果α能導出β→γ，那么當α能導出β時，α就能導出γ。這個推理過程也是合乎直覺的。

 

用希爾伯特的直覺邏輯公理來做一個小的推理練習，即證明α→α是定理。

Step1. 因為表達式中的符號可以替換，所以我們將公理（2）中的所有γ替換為α，得出

(α→β→α)→(α→β)→α→α（3）是定理。

（因為對於所有α和γ公理（2）都成立，所以當γ=α時，公理（2）顯然也成立，這可以看作公理（2）的特例應用）

Step 2. 又因為上式是定理，α→β→α 是公理，根據推演規則，得

(α→β)→α→α是定理

Step3. 再做一次特例應用，將上式中的β替換為β→α，得

(α→β→α)→α→α

Step 4. 最后將因為上式是定理，(α→β→α)是公理，根據推演規則

α→α是定理得證。

 

單個多假設命題=嵌套的單假設命題

——玄生萬物，九九歸一

 

直覺邏輯有一個重要的推論：如果定理A能導出定理B→C，那么定理A和B能導出定理C，反之亦然。該結論既可以通過公理證明，從直覺上也很容易理解。如果我們給上文中的形式系統上加一個小變化，用×符號來表示兩個定理之間的與關系AND，那么該推論可以表示為

 

如果A→B→C是定理，那么A×B→C是定理。

 

該結論可進一步拓展為，如果

A1→A2→A3→……→An→B是定理，那么

A1×A2×A3×……×An→B是定理。

 

這兩個表達式在形式系統中等價，多假設的單個命題與單假設的多個嵌套命題是可以互相轉化的。

 

引入這個符號之后，直覺邏輯中唯一的推理規則“如果α→β和α是定理，那么β也是定理”可以表示為

 

α×(α→β)→β

 

因此。與之等價的α→((α→β)→β)也是一條定理。有興趣的話可以運用直覺邏輯的推演規則證明這個結論。

 

命題映射為變量類型

——和其光，同其塵

 

下面我們來給這個推演規則做一次應用，將變量α換作命題A（命題是不可再分的表達式），β換作命題B。如此可以得到一個結論，

如果A→B是定理，A也是定理，那么B就是定理。

 

A×(A→B)→B

 

為了便於稱呼，我們給A→B這個定理起名f，表示為f: A→B，意即定理f的內容是命題A→命題B。再給A命名為p，B命名為r。上述表達式變為

 

p:A×(f:A→B)→r:B

 

下面是最重要的一步變換。由於在形式系統中，符號是最不重要的東西，我們將所有的A替換為TypeA，B替換為TypeB，上式依然是命題邏輯唯一的推演規則：

 

p:TypeA×(f:TypeA→TypeB)→r:TypeB

 

下面再把p置換為param，f置換為func，r置換為ret，上述表達式變為

 

param:TypeA×(func:TypeA→TypeB)→ret:TypeB。

 

注意，除了給定理加上名字並且替換相應符號，這個表達式與α×(α→β)→β沒有任何本質區別。我們依然可以宣稱它代表直覺邏輯唯一的推演規則：如果TypeA是定理，TypeA→TypeB是定理，那么TypeB也是定理，其中的TypeA，TypeB都是命題的名字。但是，對於程序員而言，分明會將它理解為類型系統中唯一的推演規則:

 

如果函數func的入參是類型A，返回值是類型B，那么調用時輸入類型為A的變量param，就會得到類型為B的返回值ret。

其中TypeA→TypeB 表示函數func的類型，該函數參數類型為TypeA，返回值類型為TypeB。

 

在這條規則中，加上param和func等等名字只是有助於理解，類型系統的核心規則與命題邏輯的核心規則具有完全一樣的形式

 

A×(A→B)→B

 

其中A既可以從程序的角度理解為類型，也可以從邏輯的角度理解為命題，采用不同的解釋時，對於這個表達式的解釋也會發生相應的變化。

 

這也就是計算機形式化驗證的基石—— 柯里-霍華德同構。它意味着同一套符號系統既可以解釋為程序的類型，也可以解釋為直覺邏輯的推理。

 

對於多參數的的函數而言，可以將其改造為多個單參數的函數嵌套的形式，再應用以上推演規則。例如：函數

 

fn curry(a:A, b:B) -> C{
　　return foo(a, b);
}
 
curry(x, y)

 

等效於

 

fn curry(a:A) -> B->C {
    let curried = fn(b:B) -> C {
        foo(a, b)
    };
    return curried;
} //curry函數返回一個類型為B->C的函數curried，該函數接受一個類型為B的參數，返回值類型為C
 
let func = curry(x);
func(y);    

這個過程稱為柯里化，即如果可以構造類型為A×B→C的函數，那么必然可以構造類型為A→(B→C)的函數。注意看前一節 單個多假設命題=嵌套的單假設命題 中，直覺邏輯的推論，即

 

如果可以推出定理A→(B→C)，那么可以推出定理 A×B→C

 

這個過程與程序的柯里化過程是同構的。

 

證明映射為程序

——色不異空，空不異色；色即是空，空即是色

 

對於一個程序員而言，如果他能構造一個類型為A->B的函數，則表示可以構造一個定理A->B證明，其中A是假設，B是結論。函數體從參數到返回值的步驟，等同於證明從假設到結論的步驟。如果這個函數能夠通過編譯器檢驗而無類型錯誤，則說明對應的證明是沒有邏輯謬誤的。

 

換句話說， 每一個直覺邏輯表達式都可以映射為一個函數的類型，每一個可證明的直覺邏輯表達式都可以映射為一個可以實現的函數類型。

 

在更詳細地解釋這兩套推演系統是如何對應之前，先看一張表：

 

變量名：變量類型	命題名：元命題
函數名：函數類型	定理名：定理內容
參數名：參數類型	假設名：假設內容
返回名：返回類型	結論名：結論內容
函數體	證明（proof）
類型檢查(type checker)	證明驗證(proof verifier)
庫函數	已證明的定理
函數調用	定理應用
構造函數	公理
類型推導	命題推演
類型錯誤	邏輯謬誤
……	……

 

這張表可以列得很長很長，直到我們為計算機程序中的每一個概念在直覺邏輯中找到一個對應物。甚至包括一些邊緣概念

緣於遞歸的棧溢出	緣於自引用的悖論
停機問題	哥德爾不完備

下面用例子來說明一下表中某些項的對應關系。

 

例一：證明的驗證

假設有這樣一段代碼：

struct A {
    String field;
}
 
impl A {
    fn new(field: String) -> A {
        A { field }
    }
}
 
 
fn string_implies_A(field: String) -> A {
    A::new(field)
}
 
let hypothesis: String = String::new();
let conclusion: A = string_implies_A(hypothesis);    

這個程序的結構如圖

 

 

可以看到它的核心結構是重命名了A::new()為string_implies_A，輸入一個類型為String的參數hypothesis，返回conclusion:A。

 

我們寫好這樣一段程序，交給編譯器，從編譯器的角度很好理解

• string_implies_A重命名了函數A::new(),類型是String->A；
• 輸入的變量hypothesis，類型String與string_implies_A的參數匹配，該變量用String::new（）初始化。
• 調用string_implies_A返回值類型為A，與conclusion預定義的類型相同。

編譯器會告訴我們這段代碼的類型推導過程是完全正確的。

 

但是從邏輯的角度，這個過程就變成我們寫好了這樣一段證明，交給證明器。盡管機器工作的過程完全相同，對各個符號的人為理解卻完全不同。

• 首先，string_implies_A重命名了公理A::new()，內容是String->A；
• 其次，輸入條件hypothesis，內容String與string_implies_A的假設匹配，String:new()表示hypothesis來自公理。
• 應用定理string_implies_A返回A，與預設conclusion的內容A相同。

證明器會告訴我們這段證明的命題推理過程是完全正確的。

 

上述 程序/證明的核心是string_implies_A。在兩種理解中，string_implies_A的類型String->A，既可以理解為函數string_implies_A接受參數String，返回參數A，也可以理解為定理接受假設String，返回結論A。

函數調用輸入參數的過程就是定理接收假設條件的過程。在計算機中，所有的程序都可以看作函數的組合，一個函數的返回值會用作另一個函數的參數，得到下一步返回值。在邏輯系統中，所有的證明也都可以看作定理的組合，一個定理的結論可以作為另一個定理的條件，得出新的結論。

 

當程序無法通過類型校驗時，表明相應的證明也無法通過驗證。例如，將函數主體改為

let hypothesis: String;
let conclusion: A = string_implies_A(hypothesis);

編譯器會告訴我們hypothesis沒有使用String::new()初始化，放在證明中，這相當於我們在證明中定義假設hypothesis：String時，沒有使用String::new()，即String是公理這一條件。在用自然語言寫成的非形式化證明中，這類對隱式假設的忽略是常見的謬誤，在寫程序時，忘記初始化也是常見的謬誤，但編譯器永遠不會漏掉這樣的問題。

 

再比如，將函數主體改為

let hypothesis: Double = Double::new();
let conclusion: A = string_implies_A(hypothesis);

編譯器會告訴我們hypothesis的類型與函數string_implies_A不匹配。從證明的角度來解釋，這相當於我們在證明中使用了公理Double，而定理string_implies_A的假設是String，Double不能作為使用該定理的條件。

 

例二：計算機推理

再來看看這樣一段代碼

use lib_fun::string_implies_A;
 
let hypothesis: String = String::new();
let conclusion = string_implies_A(hypothesis);

與例一相比，這個程序主要有兩個變化。一是string_implies_A不是由自己定義，而是引入的庫函數；二是conclusion沒有顯式地聲明類型，而是由編譯器進行類型推導。

 

先來看庫函數如何從兩種角度來解釋。在use lib_fun::string_implies_A中，庫函數string_implies_A代表已通過編譯，可以直接調用的函數，我們不必關心它的實現細節，編譯器會確保它的類型String -> A是可以通過類型校驗的。

 

從證明器的角度看來，string_implies_A代表已通過驗證，可以直接應用的定理。我們不必關心它的證明細節，證明器確保它所證明的定理String -> A是可以通過證明器檢驗的。

 

再來看類型推導如何從兩種角度來解釋。在let conclusion = string_implies_A(hypothesis)中，將類型為String -> A的函數string_implies_A應用於變量hypothesis: String，編譯器可以推導出conclusion的類型必然是A。用在證明里，相當於將定理String -> A應用於假設hypothesis：String，可以得出結論conclusion必然為A。

 

如果加一點變化，刪去hypothesis的定義，加上conclusion的類型

use lib_fun::string_implies_A;
 
let conclusion：A = string_implies_A(hypothesis);

編譯器會告訴我們缺少一個類型為String的變量hypothesis。開發者就會知道調用其它函數獲得這個變量，或者嘗試直接使用構造函數String::new()。

從證明器的角度來解釋，這意味着當我們想要利用String->A證明A時，證明器告訴我們缺少一個條件hypothesis: String。我們可以利用其它定理推導出String，或者使用公理String。

 

例三：計算機輔助證明

假設我們想證明前文所述的定理f：A×(A→B)→B，根據柯里-霍華德同構，這意味着我們想要構造一個類型為A×(A->B)->B的函數。我們可以一步到位，手動寫出這個函數

fn f(a:A, h:A->B) -> B {
    return h(a)
}

編譯器會告訴我們這個函數可以通過類型校驗，意即證明器告訴我們這個證明是正確的。

 

如果我們試圖證明表達式A×(B→A)→B，會發現利用現有的函數和變量，無法構造類型為A×(B→A)→B的函數，這意味着這個表達式是推導不出來的。

 

在大型數理邏輯問題中，如果我們想要證明的表達式過於復雜，人工構造函數的難度會以指數曲線上升，這時可以借助計算機的類型推導工具。

 

還是以A×(A→B)→B為例。

程序角度：

• 直接將這個類型輸入計算機，編譯器會分析出這一個函數，函數接受a: A和h: A->B兩個參數，返回B；
• 嘗試在代碼的最后一行調用其中一個參數h，即類型為A->B的函數，編譯器告訴我們，給這個函數輸入類型為A的參數就可以返回B；
• 將另一個參數a輸入該函數h，類型為A×(A→B)→B的函數構造完成。

 

證明角度：

• 直接將這個表達式輸入計算機，證明器會分析出這一個定理，定理接受a: A和h: A->B兩個假設，結論B；
• 嘗試在代碼的最后一步應用內容為A->B的定理h，證明器告訴我們，輸入內容為A的假設就可以得到B；
• 最后將a輸入該定理h，內容為A×(A→B)→B的定理得證。

 

如今的編譯器可以自動做一些類型推導，但是對於過於復雜的程序結構，還是需要手動在關鍵節點顯式指定表達式的類型；同理，證明器可以做部分自動推理，輔助人類構造證明，並驗證證明的正確性，而不是完全代替人類自動證明。計算機輔助證明工具Coq正是這樣工作的。

 

在以上所有例子中，type checker只是按照A×(A→B)→B這樣預設的法則運行，要將符號A解釋為程序的類型還是證明中的命題取決於人腦中的概念。對計算機而言，這些符號本身是沒有意義的，可以任意替換為TypeA，Apple等等。正如三段論中“蘇格拉底”的本質，也只是四個沒有任何意義的漢字符號，而不是某位偉大的哲學家其人。意義不在符號里，不在三極管與電流之中，在乎人心本身。

 

佛告須菩提：“凡所有相，皆是虛妄；若見諸相非相，即見如來。” ——《金剛經》

 

三、形式可以表示什么樣的邏輯？

低階邏輯衍生為高階邏輯

——道生一，一生二，二生三，三生萬物

 

柯里-霍華德同構表明，在直覺邏輯中，所有用形式化的方法寫成的證明，都可以解釋為一個帶類型的程序，並交給計算機驗證。類型錯誤意味着這個證明缺乏某個條件，或條件與假設不匹配。

 

然而，直覺邏輯的表達能力畢竟是有限的。例如，由於沒有“真”“假”的定義，直覺邏輯無法使用反證法，我們只能推出一個定理，而不能證明某個命題的否命題為假。但是，利用直覺邏輯的符號定義新的概念，引入新的公理，可以增加直覺邏輯的表達能力。

 

高階邏輯中新引入的概念，可以由低階邏輯中已有的法則來定義。由於篇幅所限，不能對形式邏輯的具體定義展開討論，這里依然用數學來類比。古老的四則運算系統僅包含+ - * /和（）=七個符號以及它們的運算法則，這一系統的表達能力是有限的，無法用來表示 已知正方形的面積，求其邊長 這樣的運算。

 

為了解決這一問題，數學家以乘法為基礎定義了冪運算，m的n次冪等於n個m相乘的結果。接着，數學家將冪運算的逆運算定義為開方運算，用符號√ 來表示，如此就能表示 求特定面積的正方形邊長 這樣的計算過程了。

 

隨着數學的發展，越來越多的符號和運算被發明出來，如積分，求和，階乘，等等等等，然而新符號總是有限的，不同數學家采用的符號也不盡相同，新的數學問題卻源源不斷地涌現出來，因此， 亟需一種統一的，強大的符號系統，用於表示盡可能多的數學運算。

 

上個世紀前半葉，許多數學家與計算學家都投入了這項工作，如圖靈設計的圖靈機，丘奇設計的 λ演算等等。需要注意的是，雖然圖靈機的描述使之聽起來很像一台用物理器件造出的機器，但它的本質是一個抽象的計算模型，所謂紙帶、讀寫頭等等，都是用來定義運算規則的符號。圖靈機可以有各種各樣的實現，我們可以用紙筆來執行圖靈機的運算過程，也可以嘗試用機械元件來制造一個自動運行的圖靈機（但圖靈沒造出來）；就像布爾運算是一個抽象的計算模型，我們既可以用三極管來實現它，也可以用秦始皇的人列方陣一樣。

 

所有可以用圖靈機來表示的問題稱為（圖靈） 可計算的。丘奇證明他的 λ演算和圖靈機等價，因此， λ演算是圖靈完備的。它們都是現有最強的計算模型，可以計算所有可計算問題。

 

回到邏輯系統， 直覺邏輯是最簡單的邏輯系統。在直覺邏輯的基礎上定義 True， False兩個符號和 非運算法則，就得到了一個表達能力更強的系統，我們稱之為 命題邏輯。在命題邏輯中，證明一個定理的方法不只有推出它，還可以通過證明它的否命題為假來實現。

 

在命題邏輯的基礎上引入量詞符號存在∃，所有∀，就得到了 一階邏輯。在一階邏輯中，可以寫出如下表達式：

((蘇格拉底➞人)×(∀人➞死)) (1)

((蘇格拉底➞人)×(∃人➞死)) (2)

 

表達式（1）可以推出蘇格拉底會死，表達式（2）無法推出蘇格拉底會死，在初級的直覺邏輯中，這兩種計算式的區別是無法體現的。

 

在 一階邏輯中，引入“域”的概念，則可以得到二階邏輯。在二階邏輯之上，還有高階邏輯，類型論等等等等。

 

低階邏輯中引入新的符號與推理法則，可以得到更強的邏輯系統；相應地，在表示直覺邏輯的計算機語言中，定義新的符號與函數，可以得到更強大的證明器，用於表示和證明更復雜的定理。例如，我們可以定義0，1，2，3等自然數符號，+等計算符號，再將加法運算法則，即皮亞諾引理編碼為公理。如此，就能利用證明器進行數學推導與證明了。計算機輔助證明工具Coq本身提供了很多已證明的數學定理作為庫函數，可以直接引用以輔助證明。

 

形而下者謂之器 形而上者謂之道

 十七世紀，費馬一拍腦袋寫了個猜想，順手批注說自己有個絕妙證明，可惜紙太小寫不下。

三百多年后，Andrew Wiles才以108頁的論文證明了費馬的大定理，又花了兩年時間與審稿人一起發現並解決了證明中的所有漏洞。

 

所有人都相信費馬大定理是正確的，因為人們相信Wiles和他的審稿人作為數學家的專業能力。雖然大部分人窮其一生都讀不懂Wiles的證明。

 

可數學家畢竟是人，是人就會犯錯誤。1991年，菲爾茲獎得主Vladimir Voevodsky發表了對某個命題的證明，1998年，數學家Carlos Simpson 發表了關於該命題的一個反例，卻沒有提出原論文證明中的漏洞。Voevodsky無法確證是證明出了錯還是反例出了錯，或是兩個人對某個概念的理解有微妙的偏差，數學界也不知道，他們只是默默地不再引用原論文了。類似這樣的事故促使Voevodsky決心投身形式化證明的研究，因為——

 

人們應當信任統一的，嚴格的，形式化的數學，而不是信任數學家。

 

形式化證明的好處是顯而易見的：

• 一般人不可能讀懂108頁的費馬大定理證明，但是機器可以閱讀成千上萬行形式化的證明。
• 一般人引用費馬大定理時，必須信任Wiles和他的審稿人；如果費馬大定理被形式化地證明了，就只需要信任prover，同時也是type checker——一個一般化地，被全世界專業人士反復檢驗的工具。
• 一般人驗證每一個自然語言寫成的證明時，都要一行一行地讀懂它的證明，引理，引理的證明，等等等等。對於形式化的驗證，則只需要檢驗同一個type checker的正確性。它的推理規則相較於費馬大定理證明所包含的所有推理是極簡潔的。
• Type checker在一定程度上可以自動推理，例如，著名的四色問題就是使用計算機輔助證明解決的。

 

如今，數學證明的形式化表達對於人類而言，還是過於繁瑣和晦澀，就如同過去的程序員所面對的紙帶和匯編一樣。也許有一天，形式化的證明也會被高度抽象，更加接近於自然語言，就像從機器碼到高級語言的發展歷程一樣。那時的Prover將會結合神經網絡成為新一代AI，一種既遵循大量經驗，也會依賴嚴格的、合乎邏輯的推理而產生新概念的智能，一台思考機器。

 

 

思考題：
每一個形式化的證明都可以解釋為一個帶類型的程序。那么反過來，每一個程序都可以解釋成一個證明嗎？Hello World證明了什么？