本网讯：（通讯员孙中阳）2021年2月至2021年6月，必威主办了“2021秋季学期逻辑与数学基础”系列线上讲座。本学期共举行8场报告（逻辑与数学基础系列讲座第14讲至第21讲），分别由6位海外教授、1位国内教授、1位青年学者主讲。本学期此系列讲座由必威科学技术哲学教研室程勇教授负责组织。 本学期讲座内容涵盖证明论、数学基础、描述集合论。每场报告共2小时，其中主讲90分钟，交流讨论30分钟。7场线上报告在Zoom平台举行，来自海内外的师生参加了线上报告。线下报告单独报道，线上报告集中期末报道。

2021年2月26日下午4点，逻辑与数学基础系列讲座第14讲由新加坡国立大学数学系杨跃教授线上主讲，报告题目是：“Ramsey定理，反推数学及数学基础”。新加坡国立大学讲座教授、新加坡国家科学院庄志达院士主持。此讲座的内容大致可以分为三个部分。第一个部分是预备知识。杨跃教授从可计算性角度出发分别引入可计算集和一阶算术可定义集。在反推数学中，这两类集合分别对应递归论中RCA₀和ACA₀两个算术子系统。讲座的第二部分是证明反推数学中的几个定理。在证明Ramsey定理的过程中，杨跃教授运用了两种方法，一种通过不断提纯尾巴，另一种运用了二叉树的思想。讲座的第三部分是对数学哲学的讨论，主要涉及三个观察。第一个观察是绝对混沌是不可能的。第二个观察是数学问题的解比数学问题本身层次更高。第三个观察是秩序是真实存在的，我们要不断提升自己才能观察到这些秩序。

2021年3月9日下午4点，逻辑与数学基础系列讲座第15讲由德国达姆施塔特工业大学数学系Ulrich Kohlenbach教授线上主讲，报告题目是“证明论：从数学基础到核心数学中的应用”。必威程勇教授主持，英国巴斯大学计算机科学系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定理证明器”。必威程勇教授主持，上海交通大学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的一个片段。

逻辑与数学基础系列讲座线上报告的视频经报告人授权已上传至必威bilibili官方频道上，可通过以下网址观看：

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

（编辑：邓莉萍 审稿：严璨）