本网讯（通讯员杨新宇）4月17日下午，波兰华沙大学Leszek Kołodziejczyk教授通过线上方式作了“弱基础理论上的反推数学”的学术报告。Leszek Kołodziejczyk教授的研究领域广泛，以证明论和算术理论的模型论为主，研究对象涵盖了从有界算术到二阶算术的子系统的强度不同的形式理论。本次讲座由我院程勇教授主持，德国波鸿鲁尔大学哲学系研究员Sam Sanders博士评议，线上参与者达500余人次。

本场讲座分为两部分，第一部分是对反推数学这一领域的一般性的介绍，第二部分则是对弱二阶算术RCA₀^*上的Ramsey型原则这一前沿性研究的介绍。

在第一部分中，Kołodziejczyk教授首先介绍了反推数学的研究目标——澄清证明某个数学定理所需要的公理强度，而这一目标具体通过考察二阶算术的子系统上数学定理和集合存在原则的逻辑蕴涵关系而实现。通常被考察的定理为∀X∃Yψ的形式，证明此类定理的公理强度通常与给定自然数集X计算Y的复杂性有关。

为了使听众进一步了解反推数学，Kołodziejczyk教授对二阶算术进行了简要的介绍。Kołodziejczyk教授指出，所有的通常的实际的数学都可以在全二阶算术Z₂中形式化，对于反推数学而言Z₂过强了，因此我们通常通过限制内涵公理和归纳公理到某一类集合上考虑其较弱的子系统。当我们将其限制在一阶算术可定义集上我们就得到了ACA_０，将内涵公理限制在可计算集上，归纳公理限制在可计算枚举性质上我们就得到了RCA_０。为了演示反推数学的一般研究方法，Kołodziejczyk教授向听众介绍了一个简单的例子：在RCA₀上有理数列的Bolzano-Weierstrass定理和ACA_０等价。而另一个重要的系统WKL_０的强度介于RCA_０和ACA_０之间。但另一方面，反推数学的研究发现，存在一些复杂的数学定理，其强度介于RCA_０和ACA_０之间，但却与WKL_０不可比，并且其彼此之间的强度也不可比。几个Ramsey型原则即是典型的例子。

在第二部分中，Kołodziejczyk教授介绍了比RCA_０更弱的数学理论RCA₀^*。它是通过将归纳公理进一步限制到可计算性质上，同时添加关于指数函数2^x的公理得到的。随后Kołodziejczyk教授从模型的角度介绍了RCA_０和RCA₀^*的不同，并梳理了从80年代末以来关于RCA₀^*的一些结果及其研究意义。

接下来Kołodziejczyk教授介绍了他和合作者近期对RCA₀^*上Ramsey型原则强度的研究。他们考虑了根据对无穷集的两种表示方法（无界性和双射性）所区分的正规Ramsey型原则和长Ramsey型原则。对于正规Ramsey型原则，他们利用在cut上编码集合这一工具，证明了一个强有力的模型同构定理，进而得到了一些关于正规Ramsey原则逻辑后承的保守性结果，说明了不同的正规Ramsey原则在RCA₀^*上有不同的一阶后承。对于长Ramsey型原则，他们得到了一些等价性结果。

最后，Kołodziejczyk教授简要介绍了关于RCA₀^*的其他问题的研究成果和几个公开问题。

在评论和提问环节，Sam Sanders博士提出了这样一个问题：对于RCA₀和ACA₀，其研究动机是比较直观的，而研究RCA₀^*的动机是什么呢？Kołodziejczyk教授回应道，通过对RCA₀^*的研究及其和RCA₀的比较，可以表明在数学研究中对不可计算性质的归纳是必要的。日本东北大学Keita Yokoyama教授则进一步肯定了在RCA₀^*的研究中所使用的证明论方法的优美性。程勇教授则与Kołodziejczyk教授就RCA₀^*上反推数学图景的优美性以及证明论方法的应用等问题进行了交流。

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