本網訊（通訊員陳一源）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教授給予肯定的回答。最後，主持人感謝報告人帶來的精彩講座。至此，本次講座圓滿結束。

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