本網訊（通訊員楊新宇）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₀^*上反推數學圖景的優美性以及證明論方法的應用等問題進行了交流。

（編輯：鄧莉萍 審稿：劉慧）