本網訊（通訊員陳一源）11月9日和11月16日晚，德國慕尼黑大學Helmut Schwichtenberg教授通過學術志平台做了關于“自然演繹中證明的範式”（Normal of Forms of Proofs in Natural Deduction）的兩場線上講座。第一場的主題是範式的存在性和唯一性（Existence and Uniqueness），第二場的主題是範式的複雜性（Complexity）。兩場講座分别是我院邏輯與哲學系列講座第28及29講。講座由我院程勇教授主持。兩場講座各2小時，學術氛圍活躍，來自海内外共450餘人次參加了Schwichtenberg教授的講座。

第一場講座中，Schwichtenberg教授從極小邏輯（minimal logic）出發，一步步到達主題——自然演繹中證明的範式的存在性和唯一性，講座的重點在唯一性部分，前面部分都是在為唯一性部分做鋪墊。首先，Schwichtenberg教授在第一部分引入了極小邏輯的概念，指出本次講座的主題是極小邏輯自然演繹的證明範式。何謂極小邏輯?我們通常把語義完備（有效式均可證）的命題邏輯和一階邏輯稱為經典邏輯（classical logic）。現對經典邏輯做減法，如果不允許使用雙否消去規則     （），則經典邏輯退化為直覺主義邏輯（intuitionistic logic）；再對直覺主義邏輯做減法，如果不允許使用“矛盾導緻一切”規則     （），則直覺主義邏輯退化為極小邏輯。顯然直覺主義邏輯比經典邏輯弱，極小邏輯則比前兩者都更弱。在經典邏輯中，析取連接詞和存在量詞可以分别被合取連接詞和全稱量詞加否定連接詞定義。但在極小邏輯中卻沒有這個性質。Schwichtenberg教授保留了極小邏輯中原有的析取連接詞和存在量詞，又像在經典邏輯中的那樣分别用合取連接詞和全稱量詞加否定連接詞定義了一個新的二元連接詞和量詞，取名弱析取（weak disjunction）和弱存在（weak existence）。Schwichtenberg教授又論述了極小邏輯中析取蘊含了弱析取，存在蘊含了弱存在，但反之不然。這就說明了極小邏輯中弱析取與弱存在是名副其實的“弱”，也說明了在經典邏輯中能互相定義的連接詞和量詞，在極小邏輯中未必能互相定義。

然後，Schwichtenberg教授在講座的第二和第三部分介紹了Curry-Howard對應和正規化。Schwichtenberg教授引入Curry-Howard對應的主要思想是：把推演樹和Lambda項對應起來，而如果Lambda項可以進行     歸約，那麼轉換之後會形成新的更簡潔的Lambda項，其對應的推演樹和原來Lambda項對應的推演樹相比，顯得沒有那麼冗餘。推理樹之所以有時會顯得冗餘，是因為推理樹中有一些公式，既是某個引入規則的結論，又是某個消去規則的主前提，好似做了無用功。正規化的目的就是去掉推演樹中所有這樣的公式，而不具有這樣的公式的推演也叫正規推演。Schwichtenberg教授接着證明了所有的推演都能轉換成正規推演，即所有的推演均可正規化，主要思路是利用     歸約總會進行不下去的性質。于是，證明的範式的“存在性”通過正規推演的存在得以體現。

前面提到了所有的推演均可正規化，所有推演都存在正規推演。Schwichtenberg教授在講座的第四和第五部分讨論了這樣的正規推演對任意給定的推演是否是唯一的。Schwichtenberg教授給出了肯定的答案，并給予了證明。證明的思路是我們隻需證明對任意給定的推演，不同的正規化路徑能得到相同的結果。根據Curry-Howard對應，這個問題可以轉價到Lambda轉換的終點與轉換路徑 （       歸約等規則使用的先後順序）無關上。Schwichtenberg教授先證明了幾個相關的引理，然後利用這些引理證明了最終的唯一性，由此證明的範式的“唯一性”通過正規推演的唯一性得以體現。最後，Schwichtenberg教授證明了正規推演的一個很重要的性質，子公式性質：即一個正規推演中出現的所有公式，要麼是結論的子公式，要麼是沒有被消掉的前提的子公式；而這個性質是一般推演未必具有的。

第二場講座是第一場的後續内容，在第一場講座中，已經引入了正規化思想和正規推演的子公式特征，并且對任意一個推演，盡管它的正規化過程不同，但它的正規化結果，即得到的正規推演是存在且唯一的。那麼，對于任意一個可推演的公式，都能很容易地找到一個正規化推演嗎？Schwichtenberg教授認為給每個可推演的公式尋找一個正規化推演是一件不現實的事情。Schwichtenberg教授用一個初始常元，一個一元函數符号和一個三元關系符号，給出了有關的兩個前提，然後遞歸地構造了一個公式序列           ，再詳細地證明了任何一個從這兩個前提到            的正規推演樹，它所具有的結點數與            形成的函數關系式，随着     的增加，會遠遠大于和     有關的任何一個多項式，并且               越大，與多項式的差和商也會越來越大。這就是所謂的複雜性，它讓窮盡所有公式的正規推演變得不可行，證明的範式的“複雜性”通過這個例子得以體現。然後，Schwichtenberg教授圍繞着線性雙層算術（linear two-sorted arithmetic）、序數（ordinals）和算術系統的複雜性問題展開，讨論算術系統中的複雜證明。Schwichtenberg教授介紹了算術理論的序數分析的重要結果，相關定理的證明環環相扣。

在兩場講座的互動環節，Sam Sanders博士介紹了相關的理論背景，包括希爾伯特的證明論，布勞威爾的直覺主義，經典邏輯和直覺主義邏輯的聯系，Curry-Howard對應以及強正規化。程勇教授向Schwichtenberg教授提出能否把極小邏輯的這些結論拓展到經典邏輯中去。Schwichtenberg教授指出由于經典邏輯、直覺主義邏輯和極小邏輯的強度不同，有些結論的拓展還是一個新的問題。陳波教授就講座第一部分根岑轉換（gentzen translation）内容的合法性提出疑問，因為這與通常的轉換不同；Schwichtenberg教授指出這種轉換不是唯一的，是為了引出後面的定理準備的。最後Fernando Ferreira教授評價稱Schwichtenberg教授處理序數、算術系統和快速增長函數（fast growing functions）的方式對學生來說是相當優雅的。

至此，Schwichtenberg教授關于“自然演繹中證明的範式”的兩場講座順利結束。

（編輯：鄧莉萍   審稿：劉慧）