本網訊（通訊員楊新宇）11月13日晚，瑞典哥德堡大學Graham Leigh 教授通過網絡平台作了題為“證明，真和驗證（Proof, Truth and Verification）”的講座，旨在介紹劣基證明論(ill-founded proof theory)的基本思想和當前進展。講座由我院程勇教授主持，伯明翰大學Anupam Das教授評議，線上參與者近200人次。

Leigh教授首先回顧了命題邏輯的矢列演算(sequential calculus)系統CPL，這一系統具有可靠性和完全性，對于可靠性的證明可以通過施歸納于證明的高度，對于完全性的證明則是通過證明搜索(proof search)的技術證明，即通過對一個矢列的公式分解，我們要麼可以得到該矢列的在系統中的一個證明，要麼可以構造出不滿足該序列的一個真值指派。CPL的另一個重要性質是一些規則的可允許性(admissibility)。通過證明變換(proof transform)的方法我們不僅可以證明CPL初始規則的逆規則是遞歸地可允許的，還可以證明切割(cut)規則是遞歸地可允許的，這就是著名的切割-消除（cut-elimination）定理。切割-消除具有很好的性質，邏輯學家Mints在1978年證明了切割-消除可以看作是推演空間上的連續算子。

講座的第二部分是餘-歸納(co-inductive)證明論。劣基證明(ill-founded proof)的概念很自然地出現在不同的邏輯和理論系統中，如線性時态邏輯和皮亞諾算術中。這類證明具有很好的性質：證明變換是連續的；證明的複雜性而非大小是其主要指标；便于系統的模塊化分析。Leigh教授以線性時态邏輯和皮亞諾算術為例對其進行了介紹。線性時态邏輯有兩類算子：表示命題從現在開始一直為真的算子和表示命題在下一個時刻為真的算子。通過對一個典型的線性時态邏輯證明搜索的分析，Leigh教授引入了迹(trace)和優迹(good trace)的概念，進而形式地定義了劣基證明和循環證明。通過證明搜索的方法可以證明線性時态邏輯的劣基證明系統是可靠且完全的，通過證明變換的方法可以證明切割規則在線性時态邏輯的遞歸可允許性。另一個重要的例子則是皮亞諾算術PA。皮亞諾算術的矢列演算系統是在CPL的基礎上添加量詞規則、等詞規則和歸納規則、切割規則擴展而成的。通過對更強的           算術（将歸納規則替換為有無窮多個前提的ω規則）的證明論刻畫，我們可以給出PA的序數分析：任何PA可證矢列在           算術中有不使用切割規則的高度小于序數          的證明。然        算術中的證明不具備很多良好的性質：缺少計算複雜性的信息；無法擴展到其他系統；不具備模塊化性質。另外一種思路是重新定義量詞規則，引入算術的劣基證明系統和循環證明系統。可以證明，算術的劣基證明系統強度上和真算術等價，而循環證明系統和PA等價。同時可以用和線性時态邏輯類似的方法證明劣基證明系統的切割消除定理，由此可知無切割證明不可能是循環的。

講座的最後一部分是劣基證明和序數分析之間的聯系。通過定義切割迹(cut trace)，我們可以對劣基證明指派序數。邏輯學家Afshari的研究表明，在二階算術的一個子系統上，可以證明對某個推演的序數的超窮歸納蘊含該推演的最複雜的切割規則可以被消除。這個子系統需要多強呢？Leigh教授猜想這一結論在WKL₀（弱Koing引理系統）上可證。不僅如此，通過劣基證明的切割消除的精細分析，我們有可能在WKL₀+          直到序數          的超窮歸納)上給出PA一緻性的新證明。此外，這一領域當前仍有許多未解決的問題：比如對其他的理論（如歸納定義的形式理論）的劣基證明論分析。

在講座的讨論環節，Anupam Das教授就這一領域許多未解問題的技術細節，如歸納定義的理論和高階邏輯的劣基證明論，和Leigh教授進行了廣泛深入地交流。荷蘭萊頓大學的Göran Sundholm教授就ω算術的證明搜索向Leigh教授分享了看法，程勇教授就哥德爾第二不完全性定理的一個推論——不存在有窮的無切割的矢列演算系統刻畫PA與Leigh教授進行了讨論。此外，線上的觀衆則就原始遞歸算術和WKL₀的強度比較及邏輯學家Gentzen關于PA的一緻性證明和這裡提到的一緻性證明的關聯和Leigh教授進行了交流。

最後程勇教授感謝Leigh教授帶來的精彩講座，至此，本場講座完滿結束。

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