本網訊（通訊員楊新宇）12月14日晚，荷蘭烏得勒支大學特聘教授，荷蘭皇家人文與科學院院士Albert Visser教授在線作了題為“實質層級不可判定性”的講座。講座由我院程勇教授主持，海内外250餘人次參加了本次講座。

Albert Visser教授在解釋理論、不完全性和算術的元數學等方向做出了傑出的學術貢獻。本次講座是面向學生的通識講座，講座主題圍繞“實質不可判定性”和“實質層級不可判定性”這兩個重要的理論性質，以算術理論Q和理論R為對象，證明了這兩個理論滿足上述兩性質。

講座從哥德爾第一不完全性定理開始，Visser教授首先概述了第一不完全性定理的幾種不同的形式。Visser教授指出本次講座旨在研究一般形式的不完全性/不可判定性。特别地，講座研究與不完全性/不可判定性緊密相關的形式理論，通過研究理論的元數學性質用一種更一般和抽象的視角研究不完全性現象。為此Visser教授引入了“實質不可判定理論”和“實質層級不可判定理論”的概念。一個一緻的理論T是實質不可判定的，若T所有的一緻遞歸可枚舉擴充都是不可判定的；一個一緻的理論T是實質層級不可判定的，若對所有使得T∪W一緻的遞歸可枚舉理論W，W都是不可判定的。進一步，Visser教授證明了有窮公理化的實質不可判定理論是實質層級不可判定的，由這一結論我們可以從理論Q的實質不可判定性得到其實質層級不可判定性。

而實質層級不可判定性的意義在于它和另一個重要的概念，可解釋性，有深刻的聯系。稱一個理論V解釋U，若存在一個從U的語言到V的語言的翻譯τ，使得對任何公式φ, U⊢ φ蘊涵V⊢ φ^τ。解釋在數學理論中相當常見，比如集合論可以解釋算術，實直線可以解釋歐氏平面。而利用解釋的概念，可以得到實質層級不可判定性的一個充要條件，利用這一條件，我們可以從算術出發，證明其他數學理論（比如群論）的不可判定性。為了接下來的證明需要，Visser教授還介紹了兩個重要的工具：     公式的可比性見證，具有自指性的哥德爾編碼系統。

講座的主體内容是理論Q和理論R的實質層級不可判定性。Visser教授首先介紹了理論Q，即皮亞諾算術去掉數學歸納法再加上一條公理：x = 0∨∃y(x = Sy)。由于理論Q是有窮公理化的，隻需證明其實質不可判定性。證明的思路是對于Q的一緻遞歸可枚舉擴張U，利用Q理論的   Σ₁完全性和自指的哥德爾編碼系統，構造自指語句ρ =□¬ρ         □ ρ(□是可證性謂詞)，再利用U的一緻性假設，可推出ρ是獨立于U的。再根據實質不可判定的定義可得到Q是實質不可判定的。

而理論R的情況則更為複雜。不同于理論Q，理論R不是有窮公理化的，因此我們雖然可以用證明理論Q實質不可判定的方法證明理論R是實質不可判定的，卻不能因此得到理論R的實質層級不可判定性。理論R的實質層級不可判定性的證明最初由Cobham在50年代得到，但這一證明并未公開出版。1962年Vaught給出了新的證明，Visser教授這裡提供的證明比Vaught的證明依賴的條件更少。證明的思路是對于使R∪U一緻的理論U，我們可以構造R的有窮公理化擴張F使得F∪U一緻，而利用R的實質不可判定性可以得到F的實質不可判定，進而由F的有窮公理化得到F的實質層次不可判定性，由此可知U的不可判定性，因此由定義理論R是實質層級不可判定的。證明的關鍵是F的構造，Visser教授給出了一個技術性很強而又非常精巧的構造。

Visser教授随後簡要介紹了實質層次不可判定性與其他理論性質間的關系。最後，Visser教授讨論了Trakhtenbrot定理，這一定理斷言可被有窮模型滿足的語句集和可反駁的語句集是能行不可分的。

Visser教授的講座内容清晰，證明嚴謹。在評論及提問環節，程勇教授系統梳理了Visser教授講座的内容，總結了本次講座闡述的三種重要性質的關系，并提出了三個問題：通常的能行不可分性是定義在給定理論上的，但強能行不可分概念是直接定義在謂詞邏輯上的，這樣做的動機是什麼？Trakhtenbrot定理有何應用？關于理論R研究的最重要的開問題是什麼？Visser教授指出，定義在謂詞邏輯上可以看成是定義在空理論上，這種定義和Trakhtenbrot定理關系更密切；Trakhtenbrot定理在有窮模型論領域有重要應用。Visser教授指出，在理論R的研究中最重要的開問題是理論R的解釋度的結構，這一問題是一般的，并且在更為自然的理論Q的研究中尤為重要。

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

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