本網訊（通訊員孫中陽）2022年1月14日晚，美國卡内基梅隆大學Patrick Suppes邏輯和哲學教授、美國人文與科學院Wilfried Sieg院士通過學術志平台作了題為“方法論框架：數學結構主義與證明論”的線上講座。講座由beat365体育官网程勇教授主持。

此次講座由beat365体育官网主辦，是邏輯與數學基礎系列講座第23講，世界邏輯日學術報告。來自BEAT365唯一官网校内外、海内外的老師和學生參加了此次講座。講座近3個小時，問答交流環節氣氛活躍，讨論環節一個小時。

Wilfried Sieg教授的報告内容可分為5個部分。

第一部分内容的主題是背景與概述。Wilfried Sieg教授援引聯合國教科文組織宣布世界邏輯日的決議文件，來闡明世界邏輯日的意義：旨在使得邏輯的發展史、邏輯觀念的重要性及其應用價值引起跨學科科學團體和公衆的更廣泛的注意。他指出，本報告将基于希爾伯特和伯奈斯(Bernays)的工作介紹證明論的發展史、思想觀念和實際應用。

Wilfried Sieg教授繼而引入了報告主題的曆史背景。希爾伯特和伯奈斯開創了證明論，其是數理邏輯的一個分支。證明論不僅為研究“數學證明”提供了普遍框架，而且也是一種建立具體對象和抽象概念間關聯的重要工具。 經典數學和構造性數學間的張力在希爾伯特的有限一緻性綱領中得到調和。伯奈斯在他1930年的論文《數學哲學與希爾伯特綱領》中将數學視為理想結構的科學。他的觀點強調了19世紀下半葉數學發展的方法論轉變。伯奈斯指出刻畫這種方法論轉變的三個特征：（1）集合論的發展；（2）結構化公理的出現；（3）邏輯與數學間的緊密聯系。

第二部分内容的主題是數學結構主義。Wilfried Sieg教授指出，方法論框架在元數學研究和數學實踐中均起到了重要的作用。在現代數學中使用的公理化方法，是與數理邏輯中的形式語言和邏輯演算無關。例如，群、環、域、拓撲空間這些數學結構的公理其實是它們的結構定義的特征。現代數學中的公理化方法需要一種更一般的方法論框架。Wilfried Sieg教授援引戴德金的工作說明方法論框架在元數學中的重要意義。在戴德金、希爾伯特和策墨羅看來，這種方法論框架就是邏輯。這種邏輯框架推動了元數學研究的發展。對邏輯框架的形式語義的研究推動了模型論的發展。人們研究邏輯框架的模型及其不同模型間的關系。戴德金引入了映射概念使得能夠以保持結構的方式将不同的模型聯系起來。

Wilfried Sieg教授指出，方法論框架對于元數學研究和數學理論的形式化都是重要的。在戴德金的工作中，初等數論的形式化是基于自然數的遞歸定義和歸納法的形式表示完成的。策墨羅的公理集合論系統被視作典範的邏輯框架。Bourbaki在1950年的綱領性文章《數學體系結構》中，清楚地闡述了這種從邏輯框架的角度看待數學的方式，提出了數學結構的功能，并闡明了數學結構的内涵。

第三部分内容的主題是形式化與歸約。為解決系統一緻性的問題，希爾伯特和伯奈斯在1917-1918年的講座中引入歸約性公理，将懷特海-羅素《數學原理》中的分支類型論系統轉化為一個可在其中發展出絕大部分經典數學的邏輯系統。一個核心的方法論問題是：這個系統是數學的邏輯基礎嗎；若是的話，那麼從數學到邏輯的一個哲學上令人滿意的歸結已經完成。1917年9月，希爾伯特在瑞士數學學會蘇黎世會議上重申了戴德金的觀點，即數學是邏輯的一部分。弗雷格和羅素關于數學基礎的工作也支持這一觀點。伯奈斯的綱領性建議是，将數學理論投射到一個構造性理論中，并從有限性角度研究該構造性理論，進而解決一緻性問題。然而，一緻性問題并沒有得到解決，它隻是通過一個理論投射到了另一個理論。哥德爾稱，希爾伯特有限性綱領對數學家和哲學家都是吸引人的；若其成功的話，它表明數學可歸結為一個具體而可靠的很小部分。 然而，哥德爾不完全性定理在一定意義上否定了希爾伯特綱領的初步計劃。其後，基于根岑關于一階算術的一緻性證明，哥德爾和伯奈斯擴充了有限性方法所涵蓋的範圍。伯奈斯指出，如果我們想擴大方法論框架的應用性，那麼我們就必須避免在某種意義上過于絕對地使用證明和确定性的概念。他以一個開放的視角，允許區分不同層次和不同種類的證明，并堅持語法的一緻性證明在方法論上的重要性。

第四部分内容的主題是構造性對象及其原則。為了适應歸約的目标，伯奈斯要求方法論框架必須滿足關于構造性數學對象的一個關鍵條件：數學對象不是任意給定的，而是由生成性的過程構造而成的。哥德爾和根岑獨立證明了，初等數論PA相對于直覺主義算術HA的相對一緻性。這個結論表明，直覺主義數學是有限主義數學的一個恰當的構造性擴充。那麼，方法論框架需要具備什麼樣的一般特征，才能适用于希爾伯特的構造主義綱領？語法概念如公式、證明的遞歸定義提供了一種生成性的程序。Aczel關于構造性集合論的工作為我們提供了一種一般的生成數學對象的方法。歸約是協調、統一和連接具有許多不同模型的抽象概念和被典範同構所唯一刻畫的構造性集域，并保證抽象概念一緻性的重要方法。

講座最後一部分内容的主題是證明論的應用。 數學實踐中的非形式證明在形式理論中是可形式化的。1917年，希爾伯特提出發展關于數學證明的系統理論。根岑在他1933年的論文中提出自然演算。他認為自然演算和人類真正的推理是很接近的，自然演算是數學證明的圖像，特别适合于數學證明的形式化。根岑的這篇論文指明了證明論的研究對象：數學證明。證明論的兩個核心問題是：數學證明的實際結構是什麼？如何有效的策略性地構造證明？這些是基于計算機的形式驗證和自動證明的核心問題。從20世紀80年底以來，Wilfried Sieg教授研究如下問題：邏輯框架下數學證明的良好結構，交互式自動構造證明的策略性方法，及發現自動證明的啟發性原則。解決這些問題涉及建構恰當的自然演算系統，發現邏輯有效的原則，物理實現證明搜索的機制。Wilfried Sieg教授通過分析自然演算的一些非自然特征，引入了NIC演算，描述了NIC演算的元數學結果，并讨論了其在證明搜索系統APros中的應用。Wilfried Sieg教授總結道，這些工作告訴我們如何結構化分析數學證明，如何在形式系統中表示數學證明，及如何尋找高效的自動證明方法，從而在一定意義上揭示人類心智的能力。

報告第四部分和最後部分結束後分别進行了聽衆自由讨論環節。 包括牛津大學Daniel Isaacson教授在内的四位海外學者、BEAT365唯一官网陳波教授、程勇教授及其他觀衆分别就希爾伯特綱領的實現策略與途徑、希爾伯特關于數學結構主義與證明論間的關聯的看法、證明論與遞歸論的區别、如何看待有限主義數學及嚴格有窮主義數學哲學、希爾伯特一緻性證明綱領中有限性方法的内涵、APros與其他自動證明輔助工具的比較、結構歸約的性質，構造性序數概念的定義、APros是否也适用于非經典邏輯等方面的問題與報告人進行交流，Wilfried Sieg教授詳盡清晰地一一回應了大家的問題。

最後，主持人程勇教授感謝Wilfried Sieg教授的精彩報告和讨論環節聽衆的積極參與，Wilfried Sieg教授在BEAT365唯一官网的線上學術講座圓滿結束。

（編輯：鄧莉萍   審稿：嚴璨、吳昕炜）