本網訊：（通訊員孫中陽）2021年2月至2021年6月，beat365体育官网主辦了“2021秋季學期邏輯與數學基礎”系列線上講座。本學期共舉行8場報告（邏輯與數學基礎系列講座第14講至第21講），分别由6位海外教授、1位國内教授、1位青年學者主講。本學期此系列講座由beat365体育官网科學技術哲學教研室程勇教授負責組織。 本學期講座内容涵蓋證明論、數學基礎、描述集合論。每場報告共2小時，其中主講90分鐘，交流讨論30分鐘。7場線上報告在Zoom平台舉行，來自海内外的師生參加了線上報告。線下報告單獨報道，線上報告集中期末報道。

2021年2月26日下午4點，邏輯與數學基礎系列講座第14講由新加坡國立大學數學系楊躍教授線上主講，報告題目是：“Ramsey定理，反推數學及數學基礎”。新加坡國立大學講座教授、新加坡國家科學院莊志達院士主持。此講座的内容大緻可以分為三個部分。第一個部分是預備知識。楊躍教授從可計算性角度出發分别引入可計算集和一階算術可定義集。在反推數學中，這兩類集合分别對應遞歸論中RCA₀和ACA₀兩個算術子系統。講座的第二部分是證明反推數學中的幾個定理。在證明Ramsey定理的過程中，楊躍教授運用了兩種方法，一種通過不斷提純尾巴，另一種運用了二叉樹的思想。講座的第三部分是對數學哲學的讨論，主要涉及三個觀察。第一個觀察是絕對混沌是不可能的。第二個觀察是數學問題的解比數學問題本身層次更高。第三個觀察是秩序是真實存在的，我們要不斷提升自己才能觀察到這些秩序。

2021年3月9日下午4點，邏輯與數學基礎系列講座第15講由德國達姆施塔特工業大學數學系Ulrich Kohlenbach教授線上主講，報告題目是“證明論：從數學基礎到核心數學中的應用”。beat365体育官网程勇教授主持，英國巴斯大學計算機科學系Thomas Powell博士、德國波鴻魯爾大學哲學系Sam Sanders博士、杭州電子科技大學數學系徐洪坤教授擔任與談人。講座由偉大的Hilbert計劃出發，講到Kreisel的開創性思想。Kreisel将證明論的重點從僅僅是數學理論的一緻性問題轉移到這樣一個問題上:“如果我們用有限的方法證明了一個定理，除了知道它是真的，我們還能知道什麼?”在此基礎上，Ulrich Kohlenbach引出了本次講座的核心内容：證明挖掘。緊接着，Ulrich Kohlenbach概述了證明挖掘在核心數學中的應用。在過去的20年裡，使用證明挖掘方法人們在如下領域已發現大量新的定量結果和定性結果：非線性分析，不動點理論，遍曆理論，拓撲動力學，逼近理論，凸優化，抽象柯西問題，追蹤-回避博弈。Ulrich Kohlenbach介紹了證明挖掘的應用基礎，如何将一個給定的證明翻譯成一個新的證明使得新證明是基于直覺主義邏輯，同時還使用了理想的元素。講座的最後，Ulrich Kohlenbach從凸優化、追蹤-逃避博弈、遍曆理論三個方面，具體講解了證明挖掘在核心數學中的應用。

2021年3月23日下午4點，邏輯與數學基礎系列講座第16講由德國達姆施塔特工業大學數學系Anton Freund博士線上主講，報告題目是：“良序原則和統一的Kruskal定理”。新加坡國立大學數學系楊躍教授主持，德國波鴻魯爾大學哲學系Sam Sanders博士、比利時根特大學數學系Juan P. Aguilera博士擔任與談人。 講座中，Anton Freund主要介紹了Michael Rathjen 和 Andreas Weiermann的工作——将Kruskal定理從樹擴展到一般的遞歸數據類型，并在講座的最後做了總結：良序原則連接了數理邏輯的幾個領域，尤其是序數分析、可計算理論和反推數學；通過它可得到比傳統序數分析方法更抽象和優雅的結果（例如Bachmann-Howard不動點）。

2021年4月7日上午9：30，邏輯與數學基礎系列講座第17講由美國卡内基梅隆大學哲學系、數學系Jeremy Avigad教授線上主講，報告題目是：“交互式定理證明與Lean定理證明器”。beat365体育官网程勇教授主持，上海交通大學John Hopcroft計算機科學中心曹欽翔助理教授、 中國科學院軟件研究所詹博華副研究員、北京大學哲學系王彥晶教授參加與談。講座伊始，Jeremy Avigad對交互式定理證明進行了簡要的概述。借助于計算機證明助理，數學在實踐中是可以形式化的。 使用這樣的證明助理，用戶可以構造一個形式化的公理證明。在許多系統中，這個證明對象可以單獨提取和驗證。緊接着，講座針對三類人群——數學家、邏輯學家、哲學家來探讨為什麼他們要關注這一領域。對于數學家，形式化證明助理是種可以幫助我們更好地做數學的工具。對于邏輯學家，形式化方法依賴于諸多邏輯學中的經典結果。對于哲學家，形式化方法的發展提出了一些有趣的哲學問題。講座的最後，Jeremy Avigad介紹了一個特定的定理證明器——Lean，越來越多的數學家開始使用它，并做出一些重要的成果。

2021年4月17日上午9點，邏輯與數學基礎系列講座第18講由南開大學數學系丁龍雲教授線下主講，報告題目是：“等價關系與Borel歸約”。參見此線下報告的報道：http:/info/1037/14057.htm

2021年5月18日下午4點， 邏輯與數學基礎系列講座第19講由捷克科學院數學研究所Pavel Pudlák教授線上主講，報告題目是：“從皮亞諾算術到證明複雜性”。荷蘭烏得勒支大學哲學系教授、荷蘭皇家人文與科學學院Albert Visser院士主持，新加坡國立大學數學系楊躍教授、比利時根特大學數學系Fedor Pakhomov博士擔任與談人。證明複雜性是與邏輯、計算複雜性和組合優化相關的一個快速增長的領域。報告伊始，Pavel Pudlák首先介紹了證明複雜性的起源和曆史發展。它始于20世紀初Hilbert學派的研究，其目的是證明PA的完備性與一緻性。20世紀30年代，哥德爾創造性的成果推翻了Hilbert學派的猜想，其成果主要有兩個核心要點：一是對證明進行編碼，二是構造了自指語句。20世紀70年代，伴随着計算複雜性理論的出現，人們的研究重點轉向PA的片段子理論，并發現了其弱片段與複雜性類之間的聯系。緊接着，報告對證明系統的基本概念做了介紹。一個證明系統可以是任何二元關系R（x，y）（y是x的一個證明）,并滿足以下性質：系統是可靠的；系統是完備的；二元關系在多項式時間算法中是可判定的。然後，Pavel Pudlák又介紹了來自組合優化的證明系統。 證明複雜性這一新興領域的另一個推動力來源于此。 講座的最後，Pavel Pudlák對證明複雜性這一研究領域做了總結。它不僅僅是對證明長度的研究，它包含了所有對弱形式系統及與可行性計算相關聯的系統的研究。Pavel Pudlák用一個具體的例子演示了如何使用命題證明複雜性來證明一個獨立性結果。

2021年6月15日上午9點， 邏輯與數學基礎系列講座第20講由瑞典哥德堡大學Ali Enayat教授主講，報告的題目是：“Flexible-圖靈機”。新加坡國立大學數學系楊躍教授主持，新加坡國立大學數學系Tin Lok Wong博士、浙江大學哲學系Zachiri McKenzie博士擔任與談人。講座先是簡要概述了Robinson算術、對角線引理以及哥德爾第一不完全性定理等基本内容，繼而引出了Saul A.Kripke 1961年有關Flexible圖靈機的開創性工作：令理論T是Q (Robinson算術)的遞歸可枚舉的一緻擴充，W_e是圖靈機上可編碼為自然數e的程序輸出，則存在一個程序e，對任何自然數k，理論T+W_e={k}是一緻的。緊接着，Ali Enayat介紹了W.HughWoodin于2011年引入的一種新型Flexible圖靈機，并将其與前面提到的Kripke的工作進行比較和對比。講座的最後， Ali Enayat教授介紹了自己與Rasmus Blanck合作的成果，對W.HughWoodin的定理做出了改進和增強。

2021年6月22日下午4點，邏輯與數學基礎系列講座第21講由荷蘭烏得勒支大學哲學系教授、荷蘭皇家人文與科學學院Albert Visser院士主講，報告的題目是：“循環Henkin邏輯”。比利時根特大學數學系David Fernández Duque博士主持，西班牙巴塞羅那大學哲學系Joost J. Joosten教授、清華大學哲學系俞珺華副教授擔任與談人。講座從Löb條件開始講起，并給出一種情況，Löb第三條件不成立而第二不完全性定理成立，繼而引出了講座的核心問題：Löb第三條件不成立的可證性邏輯是什麼樣子？緊接着，講座開始研究循環Henkin邏輯，在這個邏輯中，我們有Löb第一和第二條件，但Löb第三條件不成立，它體現了循環語法的選擇。在講座中，Albert Visser對循環Henkin邏輯在語法層面做了解釋，并在演繹系統中證明了一些基本事實。講座的最後，Albert Visser說明了循環Henkin邏輯可以看作是mu-Calculus的一個片段。

邏輯與數學基礎系列講座線上報告的視頻經報告人授權已上傳至beat365体育官网bilibili官方頻道上，可通過以下網址觀看：

https://space.bilibili.com/592450385/channel/detail?cid=158781

（編輯：鄧莉萍 審稿：嚴璨）