本网讯（通讯员时尚）12月21日下午，日本东北大学教授Keita Yokoyama教授通过网络平台在线作了题目为“反推数学:定理划分（Reverse Mathematics: classifying theorems）”的学术报告。讲座由我院程勇教授主持。Yokoyama教授在证明论、算术的模型论等领域做出过杰出贡献，曾受邀在2022年国际数学家大会作45分钟报告。本次讲座海内外参与者达200余人次。

Yokoyama教授的讲座以幻灯片和板书相结合的形式进行。他用简练的语言介绍了“反推数学”的历史起源——从希尔伯特纲领到哥德尔不完全定理再到哈维·弗里德曼关于”right axioms”的构想、主要的研究目的——寻找使得数学中的核心定理成立的最弱系统并对数学定理进行分类以及主要的研究框架——二阶算术语言。二阶算术相比一阶算术的语言添加了集合变元，它的递归公理和概括公理也更复杂，但是表示力更强。

反推数学的研究主要集中在二阶算术的五个重要子系统，我们称之为“Big Five”，从弱到强依次是RCA₀,WKL₀,ACA₀,ATR₀,Π¹₁CA₀. 它们可以对数学中出现的大部分定理进行分类。我们把RCA₀作为基础系统去研究其他系统与一些定理的等价性。比如在RCA₀中我们可以证明，一致连续定理是等价于WKL₀的，阿斯科利-阿采拉 (Ascoli-Arzela)定理是与ACA₀是等价的。当然，这五个理论并没有涵盖所有的数学定理，比如两种染色的二维拉姆齐定理与这五个系统中的任何一个都不等价。

之后Yokoyama教授从不同的角度展示了”Big Five”的强度差异。第一种比较的角度是通过不动点定理。每一个子系统中都存在相应的不动点定理，但可以证明它们对应的不动点定理是有严格的强弱关系的。第二种是通过可计算性的强度，可以发现它们的计算模型条件是越来越苛刻的。第三种是利用证明论考察他们的一致性的强度不同，不同大小的序数蕴含了它们各自的一致性。

最后一部分Yokoyama教授先介绍了该领域目前研究的热门问题。比如其他更复杂的数学定理是否需要更强的公理系统？上文介绍的不同衡量强度的范畴之间有何关联？是否还有其他的衡量角度？这些问题的研究不仅需要扎实的逻辑基础，还需要对数学分支的许多领域都有所了解。Yokoyama教授也展示了他与合作者在这些问题上取得的一些成果。然后Yokoyama教授为观众演示了两个在RCA₀中可证等价性命题的证明过程：WKL与极值定理的等价、,Π¹₁CA₀与艾克兰德变分原理。过程中呈现了许多反推数学中常用的方法，比如使用”fallen leaves”的概念把树结构和一个实函数对应起来。

评论互动环节，有观众与Yokoyama教授讨论了极值定理和WKL的等价性证明的细节。Yokoyama教授演示的证明比之常见的做法更加简洁，可读性更强。之后程勇教授提出两个问题。一是经典分析中是否存在独立的定理，Yokoyama教授表示目前还没有发现但他正在研究PDE中的可能出现的独立命题。二是二阶算术中决定性公理可证的最大限度，Yokoyama教授回答最高可以到S₃层级中。至此，本次讲座圆满结束。

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