本网讯（通讯员陈一源）11月30日晚，英国利兹大学Michael Rathjen教授应邀作题为“序数分析的艺术”（The Art of Ordinal Analysis）的线上讲座。讲座由我院程勇教授主持，通过学术志平台直播，来自海内外共260余人次参加了Rathjen教授的讲座。

Rathjen教授是序数分析领域的国际顶尖专家。这次讲座属于通识性讲座，主要目的是介绍序数分析的发展历程。理论的序数分析是证明论的核心领域。证明论的起源可以追溯到1900年8月8日巴黎第二届国际大会，会上希尔伯特提出著名23个数学问题，其中第二个问题是关于实数算术公理系统的一致性证明。希尔伯特在公理化几何方面的工作标志着他对公理化方法的毕生兴趣的开始。对于几何，希尔伯特提供公理的算术分析解释来解决一致性问题，从而将一致性问题归约到算术理论的一致性问题。因此，算术理论的一致性问题是数学基础的根本问题。

Rathjen教授讲座由三部分组成。讲座第一部分介绍了证明论从希尔伯特到根岑（Gentzen）的发展，算术一致性的基本问题，根岑证明的主要工具：矢列演算（sequent calculus）和切割消去（cut-elimination）。Rathjen教授指出，20世纪20年代，希尔伯特提出了一个研究计划，目的是为数学提供一个安全的基础。要做到这一点，首先要把逻辑和数学全部形式化，然后证明这些形式理论是一致的，也就是说没有矛盾。此计划要求数学理论的一致性证明具有有穷主义特征。给出数学公理系统的有穷主义一致性证明的提案被称为希尔伯特纲领。Rathjen教授认为希尔伯特纲领是一项还原工程，旨在表明：当一个经典数学命题可以用超限的方法证明时，它也可以用有限的方法证明。然而，希尔伯特所谓的形式主义并不是要消除数学实践中的非构造性存在证明，而是要维护它们。20世纪20年代，阿克曼（Ackermann）和冯·诺伊曼在希尔伯特纲领框架下致力于算术系统的一致性证明的研究。阿克曼在1924年的论文中给出了原始递归算法的二阶版本的一致性证明，它明确地对序数          使用了超穷归纳法的有限版本。1936年，在根岑（Gentzen）对皮亚诺算术的一致性证明中，序数超穷归纳的应用得到了明确的重视。根岑关于皮亚诺算术的一致性证明开创了序数分析这一重要深刻的研究领域。在理论的序数分析中，人们通过一致性证明中使用的超穷序数来对理论进行分类，这些序数衡量了理论的“一致性强度”和“计算能力”。

在对根岑有关技术上工作的介绍中，Rathjen教授引入了根岑的矢列演算（sequent calculus）并介绍了矢列演算的若干规则。一个矢列，非正式地，可以说成是描述一组公式的有限析取与另一组公式的有限合取形成的逻辑后承关系的一种方式。那么什么样的矢列演算具有一种非常好的性质——子公式特征，即演算中出现的每一个公式，均是矢列演算结果中出现在前件或者后件中公式的子公式？Rathjen教授回答道，只要矢列演算中不使用切割（cut）规则，就可以使矢列演算具有子公式特征，并且任何一个矢列演算都能转换为不使用切割规则的演算，这个过程叫切割消去（cut-elimination）。最后Rathjen教授介绍了切割消去方法在皮亚诺算术系统的一致性证明中的应用。

讲座第二部分主要讲二阶算术子系统的一致性证明。Rathjen教授介绍了序数分析另一重要的工具：序数表示系统（ordinal representation systems）及其应用。最后Rathjen教授概述了序数分析从1920年代直至当今的研究进展、主要成果及当前的主要困难。

讲座第三部分主要讲序数分析的应用，主要体现在以下几个方面：构造性的一致性证明（constructive consistency proofs），组合独立性问题（combinatorial independence results）和可证函数的分类（classification of provable functions）。

Rathjen教授的报告近2小时，内容丰富，结构清晰，主旨宏大。在提问环节，程勇教授向Rathjen教授提问道“序数分析的切割消去和序数表示系统这两个工具对于理论的一致性证明而言，是否必不可少，有无替代方法？”Rathjen教授指出已知的序数分析方法都与构造某种序数表示系统有关，不使用序数表示系统的方法是全新的方法。程勇教授接着就序数分析方法是否可以解决其它领域不能解决的问题向Rathjen教授提问，Rathjen教授给予肯定的回答。最后，主持人感谢报告人带来的精彩讲座。至此，本次讲座圆满结束。

（编辑：邓莉萍 审稿：刘慧）