本網訊（通訊員：程勇）應beat365体育官网邀請，世界著名邏輯學家、數學家、國際證明論研究領軍人物、國際符号邏輯協會主席（2016-2018）、德國達姆施塔特工業大學數學系主任UlrichKohlenbach教授于5月6日至11日訪問BEAT365唯一官网。訪問期間Kohlenbach教授在弘毅學堂、beat365体育官网、數學與統計學院分别做了學術報告，并與我校師生開展了一次專場交流會。參加Kohlenbach教授系列報告的有來自beat365体育官网、弘毅學堂、數學學院、物理學院的師生和來自外省的博士生、博士後、教師等。

5月7日，Kohlenbach教授在beat365体育官网作了題為“Truth and Proof: from Paradoxes in Logic to Science”的弘毅學堂學術論壇第二十一期報告。

報告從著名的說謊者悖論談起。若說謊者語句有确定的真值，在經典邏輯中我們可從說謊者語句導出矛盾。在簡要介紹哲學家、邏輯學家對此悖論的解決方案後，Kohlenbach教授重點介紹邏輯學家如何通過恰當的形式化說謊者悖論得到現代邏輯領域一些重要深刻的結論：如哥德爾不完全性定理、塔斯基真不可定義定理、丘奇不可判定定理。在引入數論的形式系統皮亞諾算術（PA），介紹哥德爾算術化、定點定理、真謂詞的定義等重要方法工具後，Kohlenbach教授給出塔斯基真不可定義定理的證明及哥德爾不完全性定理的證明概要。哥德爾證明了哥德爾語句在算術标準模型下為真，但在PA中不可證。哥德爾的證明使用了元數學的方法，哥德爾語句是人工虛構的，沒有實在的數學内容。Kohlenbach教授介紹了一個在PA中不可證但有實在數學内容的關于初等數論的真命題：Goodstein定理。

希爾伯特綱領希望發展一種關于證明的理論用以證明在證明數學中有限組合定理時我們可以避免使用超窮方法和非構造性證明。特别的，希爾伯特綱領期望用有限性方法證明數學理論的一緻性。哥德爾第二不完全性定理表明希爾伯特綱領關于一緻性證明的目标無法完全實現。然而，過去幾十年的證明論研究表明，絕大多數經典數學中組合定理的證明可以避免使用超窮方法和非構造性證明。接着，Kohlenbach教授重點解釋證明挖掘方法是如何實現希爾伯特綱領的部分目标。證明挖掘的思想源于邏輯學家G.Kreisel的一個經典問題：給定一個關于命題T的證明，除了知道命題T為真外，我們還可從此證明中得到哪些關于命題T的新信息？證明挖掘的目标是：給定定理T的一個非構造性證明P,我們期望通過分析證明P得到關于命題T的解的可計算性界限、證明的算法、構造性的新證明等信息，通過減掉某些假設概括推廣原定理。接着，Kohlenbach教授通過兩個簡單的例子說明如何從給定的非構造性證明通過應用證明挖掘方法得到關于證明的新結論。之後Kohlenbach教授介紹了證明挖掘方法在計算機科學和數學中的應用。Kohlenbach教授總結道，現代證明挖掘方法的發展表明希爾伯特綱領的部分目标是可以實現，如從經典數學的絕大多數證明中我們可以提取關于證明的計算内容。

報告的最後，Kohlenbach教授簡要介紹了現代邏輯在哲學、計算機科學和數學中的應用。Kohlenbach教授以2014年奧地利著名雜志“Profil”上的标題結束報告：Logic is the most important science in the world!

在提問交流環節，學生們就如下方面問題與Kohlenbach教授進行了交流：經典邏輯與辯證邏輯、哥德爾定理與密碼學、人類智能與機器智能等。從黑格爾、庫恩到希爾伯特、哥德爾，從經典邏輯到非經典邏輯，從密碼學、複雜性理論到計算性理論，從圖靈機到量子計算機，Kohlenbach教練娓娓而談，細緻答疑，展現了淵博的學識和精湛的學術功底。最後，報告在德國式鼓掌中結束。

5月8日，Kohlenbach教授在beat365体育官网作了題為“Finitism and Constructivism in Philosophy of Mathematics revisited”的報告。

在過去15-20年間，G. Kreisel的證明提取思想在證明論中得到快速發展。本報告讨論證明論新發展的哲學涵義，闡釋證明論的新進展如何為諸如“構造性推理”，“有窮主義”，“理想元素”，“直謂主義”，“内涵與外延的同一性”等概念提供新的視角，更新我們對這些概念的認識，及支持一種更現實的數學哲學方法。報告首先介紹了數學基礎的三大哲學流派：柏拉圖主義、直覺主義、形式主義。這些數學基礎哲學流派對現代數學和計算機科學的發展産生了重要深遠的影響。不同的數學基礎哲學流派可發展出不同的數學：例如柏拉圖主義下的超窮集合論研究，直覺主義下的構造性數學研究。本報告旨在結合證明論研究的最新進展給出柏拉圖主義和直覺主義的形式主義解讀。在這種解讀下，數學中理想元素的本體論地位不再是最重要的問題，證明論的研究表明，雖然這些理想元素對于證明某些數學定理很有用，但對于證明某些命題而言這些理想元素不是不可或缺的，而是可以避免使用的。特别的，教授以weak Königs lemma（WKL）和The Fan principle為例為上述觀點作辯護。WKL稱任意無窮二叉樹都有無窮分支。WKL是非有限的、非能行的規則。The Fan principle是WKL在直覺主義邏輯中對應的構造性規則。在經典邏輯中WKL和The Fan principle是等價的；但在直覺主義邏輯中，The Fan principle并非蘊涵WKL。證明論的進展表明，基于很多初等數論（分析）的形式系統，在證明算術命題時我們可以避免使用WKL；進一步，基于一些恰當的直覺主義分析的形式系統，在證明算術命題時我們也可避免使用The Fan principle。報告結束後，部分師生和Kohlenbach教授作了進一步交流。

5月9日，Kohlenbach教授和來自beat365体育官网、弘毅學堂、數學學院的學生進行了一次專場交流。參加交流的師生就如下方面的問題與教授進行了交流：哥德爾完全性定理、哥德爾不完全性定理、算術的非标準模型、非标準分析、希爾伯特綱領、哥德爾綱領、德國留學入學要求等。Kohlenbach教授耐心細緻的回答了師生們的問題。兩小時的讨論氛圍輕松愉快。

5月10日，Kohlenbach教授在數學與統計學院作了題為“Proof-theoretic Methods in Nonlinear Analysis”的數學報告。數學與統計學院院長趙會江教授參加并主持報告。Kohlenbach教授首先介紹了希爾伯特綱領：發展證明論用以證明在證明有限組合命題時，超窮、非能行的方法原則上是可以避免使用的。在介紹邏輯學家G. Kreisel的經典問題後，Kohlenbach教授闡釋證明挖掘的思想：給定定理T的一個非構造性證明P,我們期望通過分析證明P得到關于命題T的解的可計算性界限、證明的算法、界限的全局獨立性等新信息。證明挖掘的核心邏輯工具是哥德爾的函數解釋方法及其擴充版本。Kohlenbach教授指出，過去20年的研究表明，證明挖掘方法導緻發現很多數學領域中新的定量結果和定性的全局結果。因時間有限，Kohlenbach教授重點介紹了證明挖掘方法在非線性分析凸優化、遍曆理論、博弈論、抽象柯西問題等領域中的應用。最後Kohlenbach教授總結了證明挖掘方法在過去20年中在分析各領域的發展：如數論、組合學、非線性分析、固定點理論、遍曆理論、拓撲動力學、近似理論、抽象柯西問題、凸優化。Kohlenbach教授指出，這些應用成果展現了現代邏輯對數學的用處和貢獻。報告結束後，部分老師和Kohlenbach教授作了進一步交流。

參加報告師生都表示有所收獲。參加弘毅學術論壇報告的聽衆指出，從報告中可感受到邏輯學家探索基礎問題的理論勇氣和追求嚴謹、精确、深刻的學術精神。參加哲學報告的聽衆指出，參加報告前以為數學哲學就是讨論數學對象是否存在的形而上學問題和人類心智如何能認識數學對象的認識論問題，參加報告後認識到科學哲學研究不僅僅是囿于書房的思辨，而是需要結合科學發展的最新成果反思并更新和深化對傳統哲學問題和觀點的理解。參加數學報告的數學學院老師指出，很多困難問題的收斂性證明都是非構造性的，聽完報告感覺這些難問題可能用邏輯來做會比較簡單。正如Kohlenbach教授在報告中指出，不論基礎還是應用研究，如果現代邏輯研究不能對哲學、數學、計算機科學産生積極影響，那麼現代邏輯對人類智慧的影響就是極其有限的、是不到位的。Kohlenbach教授的系列報告讓聽衆深切感受到現代邏輯已經并将持續對哲學、數學和計算機科學産生深刻影響。

（攝影：宋柏楊     編輯：鄧莉萍     審稿：劉義勝）