本網訊（通訊員時尚）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₃層級中。至此，本次講座圓滿結束。

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