本网讯（通讯员：程勇）应威斯尼斯人wns579邀请，世界著名逻辑学家、数学家、国际证明论研究领军人物、国际符号逻辑协会主席（2016-2018）、德国达姆施塔特工业大学数学系主任UlrichKohlenbach教授于5月6日至11日访问武汉大学。访问期间Kohlenbach教授在弘毅学堂、威斯尼斯人wns579、数学与统计学院分别做了学术报告，并与我校师生开展了一次专场交流会。参加Kohlenbach教授系列报告的有来自威斯尼斯人wns579、弘毅学堂、数学学院、物理学院的师生和来自外省的博士生、博士后、教师等。

5月7日，Kohlenbach教授在威斯尼斯人wns579作了题为“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教授在威斯尼斯人wns579作了题为“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教授和来自威斯尼斯人wns579、弘毅学堂、数学学院的学生进行了一次专场交流。参加交流的师生就如下方面的问题与教授进行了交流：哥德尔完全性定理、哥德尔不完全性定理、算术的非标准模型、非标准分析、希尔伯特纲领、哥德尔纲领、德国留学入学要求等。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教授的系列报告让听众深切感受到现代逻辑已经并将持续对哲学、数学和计算机科学产生深刻影响。

（摄影：宋柏杨     编辑：邓莉萍     审稿：刘义胜）