您所在的位置: 首页  >  学术研究  >  学术报道  >  正文

比利时根特大学Andreas. Weiermann教授来公司作“具体不完全性”系列讲座

点击次数:  更新时间:2023-08-08

本网讯(通讯员 杨新宇)7月31日至8月4日,应公司程勇教授邀请, 比利时根特大学数学系Andreas Weiermann教授来公司振华楼B214作了连续五场“具体不完全性”的系列讲座。讲座形式采用线上线下混合形式,通过Bilibili和Zoom平台向海内外观众直播,每场讲座平均超过350名观众参与,本系列讲座由程勇教授主持。著名逻辑学家Harvey Friedman也在Zoom平台参与了讲座。

Andreas. Weiermann教授是国际知名逻辑学家,是证明论和具体不完全性领域的领军人物,本系列讲座以证明论及序数分析的进路介绍具体不完全性,从证明论的基本结果出发,以可证递归函数的分层定理为工具,证明了Paris-Harrington和Friedman等构造的组合语句相对于Peano算术的不可证性,并讨论了从可证性到不可证性的“相变”(phase transition)问题。

在第一场讲座中,Weiermann教授回顾了数理逻辑的发展史,将具体不完全性研究置于数学基础研究的关键位置,突显了该领域的重要意义。随后Weiermann教授回顾了谓词逻辑的Cut-elimination定理这一经典结果,为之后的讲座作了技术准备。

在第二场讲座中,Weiermann教授讲授了Peano算术的证明论。Weiermann教授将不超过ϵ0的良序以有穷数列的哥德尔编码表示,从而证明了对于任意小于ϵ0的序数的归纳原则在Peano算术中都是可证的。基于这一事实,Weiermann教授证明了对于递归函数的Hardy分层,下标小于ϵ0的Hardy函数在Peano算术中都是可证递归的,即Peano算术可以证明其是全函数。另一方面,下标为ϵ0的Hardy函数却不是可证递归的。为了建立这一结果,Weiermann教授通过对添加Buchholz控制算子的无穷推演形式的Peano算术的序数分析证明了归约引理(Reduction Lemma), 进而得到了Hardy函数相对于Buchholz控制算子的有界性。

在第三场讲座中,Weiermann教授给出了Paris-Harrington语句不可证性的完整证明。与文献中已有的经典证明不同,Weiermann教授直接在序数标记(ordinal notation)上应用Ramsey理论,以序数的秩为工具,构造了一个巧妙的染色函数,得到了Hardy函数相对于Paris-Harrington函数的有界性。 由下标为ϵ0的Hardy函数非可证递归这一结论得到了Paris-Harrington语句不可证性。

在第四场讲座中,Weiermann教授基于下标等于ϵ0的Hardy函数非Peano算术可证递归这一结论证明了Friedman式的若干组合语句(Hydra博弈的必胜性(H)、ϵ0的缓慢良序性(SWO)、有穷树的Kruskal定理(FKT))相对于Peano算术的不可证性。并且Weiermann教授还基于Hydra博弈的必胜性的不可证性证明了Goodstein序列终止性的不可证性。

在第五场讲座中,Weiermann教授讨论了上一讲中得到的不可证语句的“相变”问题:即若某个特定的组合数学定理附带一个递增函数为参数,这个函数增长速度快到何种程度可以使其在Peano算术中不可证。Weiermann教授以解析组合学(analytical combinatoric)和复分析为工具,讨论了组合语句H、SWO和FKT的相变问题。

本系列讲座深入浅出,既易于一般的数理逻辑学习者入门具体不完全性这一领域,又深刻诠释了数理逻辑同数学其他领域的密切联系,反映了不可证现象背后的数学本质。在一些经典结果的证明上,Weiermann教授往往另辟蹊径,将序数这一工具使用得出神入化,令人耳目一新、拍案称奇。

(编辑:邓莉萍   审稿:严璨)