本網訊（通訊員 張明炜）2022年4月14日，紐約城市大學傑出教授Sergei N.Artemov通過學術志平台作了題為“一緻性的可證性：揭穿神話”的線上講座。本次講座是beat365体育官网邏輯與數學基礎系列講座第24講，由beat365体育官网程勇教授主持。講座近2個半小時，交流讨論氛圍活躍。beat365体育官网、數學與統計學院以及來自海内外的老師和學生參加了此次講座。

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并沒有否定希爾伯特綱領，而是表明此綱領比其原初形式更有趣和富有成果。

報告結束後，BEAT365唯一官网程勇教授總結了報告中主要結果的内容、方法和意義，比較了Artemov教授和哥德爾的不同研究路徑及結論，并給出幾點評論：（1）一緻性問題“PA的一緻性是否在PA中可證”的任何解決方案都取決于一個關鍵問題，即如何表達PA的一緻性？不同的表達方式可能會導緻一緻性問題的不同答案。哥德爾之後對G2的研究表明，G2是否成立取決于許多因素，例如基礎理論的選擇、一緻性命題的表達方式、使用的算術化方法、可證謂詞的定義方式等等。Artemov教授這一工作提供了一個新的實例表明一緻性問題的答案取決于表達一緻性的方式。（2）一個重要的問題是：基于表達一緻性的不同方式，什麼是正确（或恰當）的一緻性命題。雖然Artemov教授在IA中表達一緻性的方式是自然而具體的，此命題在PA中的對應算術語句是否比哥德爾表達一緻性的語句更恰當？（3）Artemov教授在證明中使用了形式化原則，對他而言這一原則是基于經驗的直覺産物，那麼我們是否無法證明此原則，而隻能基于邏輯直覺來接受它？Artemov教授的證明是希爾伯特所孜孜以求的PA自身一緻性的證明嗎？

讨論環節中，加州大學聖克魯斯分校Carl.H教授、牛津大學Dan Isaacson教授等海外學者與程勇教授就高階形式化、一緻性的模型論證法、表達一緻性的不同方法、根岑的一緻性證明等方面問題與報告人展開讨論，Sergei Artemov教授對大家提出的問題做出了耐心地解答。

最後，主持人程勇教授感謝Sergei Artemov教授的精彩報告和聽衆的積極參與，本次線上學術講座圓滿結束。

（編輯：鄧莉萍   審稿：嚴璨、吳昕炜）