本網訊（通訊員 楊新宇）6月7日晚，維也納科技大學青年學者Juan P. Aguilera博士通過學術志平台作了題為“可靠性譜系（聚焦于         ）”(Soundness Spectrum(with particular focus on         ))的線上講座。本次講座由我院程勇教授主持，海内外380餘名聽衆參與本次講座。

首先程勇教授向聽衆介紹了主講人，Aguilera博士是優秀青年學者，他目前擔任多個大學的研究職位，他的研究領域涉及數理邏輯的許多分支，他的博士論文獲得了來自國際邏輯、語言與信息協會、奧地利數學協會和德國數理邏輯協會的多個獎項。

傳統序數分析依賴于序數表示系統，在研究具有更高複雜性理論的證明論強度時遇到瓶頸。Aguilera博士的講座提出了一種研究序數分析的更抽象的框架，在其中用比序數更抽象的對象替代序數。這種框架提供了一種将傳統序數分析擴展到具有更高複雜度的對象的一般方法。

Aguilera博士的講座從序數分析的經典結論開始。 對于一個遞歸可枚舉理論T且T是ACA₀的擴張，經典序數分析關注可證遞歸良序的上确界——          ，如        。          可以看作是對理論T的          真後承的刻畫。一個自然的問題是：能否定義          來刻畫理論T的          後承。然而困難是序數并不能完成這一任務，我們需要使用更抽象的對象——dilator。

Aguilera博士對dilator的定義使用了範疇論語言，dilator是滿足一定條件(對正向極限(direct limit)和拉回(pullback)交換)的序數範疇上的函子。我們可以用實數編碼一個dilator。因此          可以定義為：最小的dilatorD使得對于任意dilatorF，若T⊢ “Fis adilator”，則F可以嵌入到D中。進而我們可以證明對于          -可靠的理論T，          存在并且是遞歸的。而對于          -不可靠的理論T，我們雖然無法定義          ，但卻可以用序數去刻畫。此時存在拟dilatorD使得T⊢ “D is a dilator”但實際上D不是dilator，這就意味着存在序數α 使得D(α)不是序數，最小的滿足這一性質的序數記為          。

講座的重心是對          的證明論分類。Aguilera博士給出了如下的可靠性譜系：（A）          當且僅當           當且僅當T是          -不可靠的；（B）          是非零遞歸的當且僅當          ≤          當且僅當T是          -可靠但是Boole(          -不可靠的；（C）          是非遞歸的當且僅當          ≤        當且僅當T是Boole(          -可靠但是        -不可靠的；（D）          ≤          當且僅當T是          -可靠的。

進而Aguilera博士證明了          形如          (即          )并且是          -可定義的。一個開問題是對于任何滿足以上兩個性質的序數α, 是否存在一個          的遞歸可枚舉擴張T使得          恰好為α，該問題被稱為“          譜系猜想”。在ATR₀中可以證明，若          譜系猜想不成立，則二階算術是一緻的。因此        譜系猜想與二階算術相容。

最後，Aguilera博士讨論了          以及          的情形。此時我們需要比dilator更抽象的對象——ptyx。一個0-ptyx是一個序數，而(n+1)-ptyx是從n-ptyx範疇到良序範疇的滿足對正向極限和拉回交換的函子。基于ptyx的概念，我們可以類似地定義          。類似于          的情形，我們可以定義          并且得到          的可靠性譜系。

在提問環節，山東大學哲學與社會發展學院梁飛副教授提出了兩個問題：1.這種分類從證明論的視角有什麼具體的意義？2.本次講座的主題能否與結構證明論建立聯系？

對于第一個問題，Aguilera博士指出          和          的情形和熟知的          情形有很大的不同，證明論學家通常關注的是可靠的理論，但在          和          的情形中不可靠的理論扮演了關鍵的角色，這是非常有趣的，為我們展現了深刻而優美的圖景。另外，          和          不可靠的理論與ZFC的擴張有着密切的聯系，可以期待未來在這方面的應用。對于第二個問題，Aguilera博士指出這次講座的主題主要基于無窮證明論的傳統，而結構證明論關注的是有窮的證明結構，比如cut-free證明的複雜性，但無窮證明論關注的是能否可證而并非實際證明如何。

程勇教授也提出了三個問題：1. Aguilera博士是否認為          譜系猜想成立？2. 本次講座中使用的dilator和通常的序數表示系統的聯系；3. Aguilera博士是否考慮過将這一技術應用于Rathjen教授提出的關于确定          -comprehension理論的證明論序數的開問題。對于第一個問題，Aguilera博士認為有證據表明          譜系猜想不成立，但不排除其成立的可能；對于第二個問題，Aguilera博士指出在同構意義上dilator可以看作一種序數表示系統；對于第三個問題，Aguilera博士表示尚未考慮過這一應用。

最後，程勇教授感謝Aguilera博士帶來的精彩講座。至此，本次講座圓滿結束。

（編輯：鄧莉萍   審稿：嚴璨）