本网讯（通讯员 张明炜）2022年4月14日，纽约城市大学杰出教授Sergei N.Artemov通过学术志平台作了题为“一致性的可证性：揭穿神话”的线上讲座。本次讲座是biwn必赢逻辑与数学基础系列讲座第24讲，由biwn必赢程勇教授主持。讲座近2个半小时，交流讨论氛围活跃。biwn必赢、数学与统计学院以及来自海内外的老师和学生参加了此次讲座。

Artemov教授首先概括了报告的主要内容。他在此报告中驳斥了一个流行的观点，即认为形式系统自身的一致性是不可能在此形式系统内得到证明的。Artemov教授在非形式算术（IA）中以一种不同于哥德尔的方式表达皮亚诺算术（PA）的一致性，在IA中证明了此一致性命题，并指出此证明是可在PA中形式化的。

希尔伯特提出PA的一致性是否在PA中可证的问题。哥德尔通过算术化方法用一个算术语句来表达PA的一致性，其第二不完全性定理（G2）称：若PA是一致的，则Con(PA)在PA中不可证，其中Con(PA)是文献中常用的表达PA一致性的算术语句，其称对任意的x,x 不是0=1的证明的编码。形式化原则（FP）断言：基于PA公理的任何严格的推导都可以在PA中形式化。基于G2和FP，人们普遍认为在形式系统内部证明此形式系统的一致性是不可能的。Artemov教授接受G2和FP，但认为由这两者并不足以得出：PA的一致性证明不可能在PA中形式化。他在IA中证明PA的一致性，并指出IA中的此证明可以在PA中形式化。

Artemov教授的论证分为两步。首先，他在IA中以如下自然的方式表达PA的一致性：任何PA的有限推导序列都不包含公式0=1；并在IA中给出此一致性命题的严格数学证明。这一步他使用的关键工具是真定义（partial truth definition）。其次，他表明此证明在PA中是可形式化的。此步他使用了形式化原则以及selector技巧，即寻找一个原始递归函数s(x)使得对任意x，s(x)是“x不是0=1的证明”在PA中的一个证明的编码。基于FP，他指出我们可在PA中证明：对任意x，s(x)是“x不是0=1的证明”的证明。

Artemov教授论证的新颖点在于：用一种不同于Con(PA)的方式给出PA一致性的新定义，并使用了一种新的证明方法：selector方法。Artemov教授通过四个例子来说明这一方法的思想及如何使用它。他指出selector方法在数学实践中被广泛使用，但却一直被排除在传统证明论之外。Artemov教授指出，G2是先在PA中给出PA一致性的形式化语句，再在PA中证明此语句不可证；而他的方法是先基于他的一致性新定义在IA中给出PA一致性的证明，再在PA中形式化此证明，但此形式化证明并不是Con(PA)在PA中的推导。因此Artemov教授的结论与G2并不矛盾。

Artemov教授总结道：这一工作挑战了传统的教条，即认为形式系统中不存在关于自身一致性的证明；并在一定意义上证实了哥德尔的观点：G2并没有否定希尔伯特纲领，而是表明此纲领比其原初形式更有趣和富有成果。

报告结束后，武汉大学程勇教授总结了报告中主要结果的内容、方法和意义，比较了Artemov教授和哥德尔的不同研究路径及结论，并给出几点评论：（1）一致性问题“PA的一致性是否在PA中可证”的任何解决方案都取决于一个关键问题，即如何表达PA的一致性？不同的表达方式可能会导致一致性问题的不同答案。哥德尔之后对G2的研究表明，G2是否成立取决于许多因素，例如基础理论的选择、一致性命题的表达方式、使用的算术化方法、可证谓词的定义方式等等。Artemov教授这一工作提供了一个新的实例表明一致性问题的答案取决于表达一致性的方式。（2）一个重要的问题是：基于表达一致性的不同方式，什么是正确（或恰当）的一致性命题。虽然Artemov教授在IA中表达一致性的方式是自然而具体的，此命题在PA中的对应算术语句是否比哥德尔表达一致性的语句更恰当？（3）Artemov教授在证明中使用了形式化原则，对他而言这一原则是基于经验的直觉产物，那么我们是否无法证明此原则，而只能基于逻辑直觉来接受它？Artemov教授的证明是希尔伯特所孜孜以求的PA自身一致性的证明吗？

讨论环节中，加州大学圣克鲁斯分校Carl.H教授、牛津大学Dan Isaacson教授等海外学者与程勇教授就高阶形式化、一致性的模型论证法、表达一致性的不同方法、根岑的一致性证明等方面问题与报告人展开讨论，Sergei Artemov教授对大家提出的问题做出了耐心地解答。

最后，主持人程勇教授感谢Sergei Artemov教授的精彩报告和听众的积极参与，本次线上学术讲座圆满结束。

（编辑：邓莉萍   审稿：严璨、吴昕炜）