本网讯（通讯员杨新宇）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教授带来的精彩讲座。至此，本次讲座圆满结束。

（编辑：邓莉萍  审稿：刘慧）