本网讯（通讯员孙中阳）2022年1月14日晚，美国卡内基梅隆大学Patrick Suppes逻辑和哲学教授、美国人文与科学院Wilfried Sieg院士通过学术志平台作了题为“方法论框架：数学结构主义与证明论”的线上讲座。讲座由biwn必赢程勇教授主持。

此次讲座由biwn必赢主办，是逻辑与数学基础系列讲座第23讲，世界逻辑日学术报告。来自武汉大学校内外、海内外的老师和学生参加了此次讲座。讲座近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教授在内的四位海外学者、武汉大学陈波教授、程勇教授及其他观众分别就希尔伯特纲领的实现策略与途径、希尔伯特关于数学结构主义与证明论间的关联的看法、证明论与递归论的区别、如何看待有限主义数学及严格有穷主义数学哲学、希尔伯特一致性证明纲领中有限性方法的内涵、APros与其他自动证明辅助工具的比较、结构归约的性质，构造性序数概念的定义、APros是否也适用于非经典逻辑等方面的问题与报告人进行交流，Wilfried Sieg教授详尽清晰地一一回应了大家的问题。

最后，主持人程勇教授感谢Wilfried Sieg教授的精彩报告和讨论环节听众的积极参与，Wilfried Sieg教授在武汉大学的线上学术讲座圆满结束。

（编辑：邓莉萍   审稿：严璨、吴昕炜）