本網訊（通訊員 時尚） 4月26日晚，荷蘭烏得勒支大學邏輯教授、哲學邏輯雜志主編Rosalie Lemhoff教授應邀通過網絡平台做了主題為“論普遍證明理論中證明系統的存在性”的線上講座。講座由我院程勇教授主持，廈門大學哲學系林哲副教授作與談人。來自國内外的200餘名聽衆參加此次線上講座。

首先由程勇教授介紹主講人。Lemhoff教授在數學基礎、證明理論等領域作出了傑出貢獻。本講座旨在讨論具有良好性質的證明系統的存在性，Lemhoff教授以序列演算為例讨論中間邏輯中的良好演算的存在性。Lemhoff教授先引入序列演算，再引入良好序列演算的記号定義，最後給出一個可行的判别方法和目前已獲得的研究成果。

Lemhoff教授首先介紹了證明論的起源和發展并引出了序列演算。她從希爾伯特在1900年國際數學家大會中提出的23個重要數學問題講起。其中的第二個問題就是證明算術公理的一緻性問題。一緻性直觀上講就是自洽，不自相矛盾，即在一個證明系統中不會推演出謬論。這個問題在哥德爾1931年發表的不完全性定理得以解決。雖然結果看似與希爾伯特最初的猜想相違背，但引起了此後證明論的不斷衍生和發展。然後她介紹了大家熟悉的自然演繹。自然演繹有許多不同的形式系統，Lemhoff教授介紹了教學中常見的Łukasiewicz第三系統和隻有一條公理加分離規則的Meredith公理系統。結構證明論中的主要研究方向之一是證明的正規化問題。所謂一個證明是正規的，是指它中間沒有“彎路”，直觀上就是證明中沒有重複和冗餘的部分。Gentzen, Prawitz等人先後分别證明了直覺主義邏輯和經典主義邏輯的正規化定理。Gentzen在證明的過程中發現自然演繹的工具并不方便，于是創建了序列演算。序列演算的美觀和易用性使得它成為了普遍證明論和結構證明論中的一種重要證明系統，我們本次講座也是使用該證明系統。之後Lemhoff教授介紹了經典主義命題邏輯中的序列演算的兩條公理：原子公理和矛盾公裡；四條結構規則：兩個弱化規則和兩個收縮規則；對于每一個聯結詞還有對應的兩條操作規則。注意她讨論的序列演算         的兩邊是公式集，所以我們無須考慮它們的順序問題，于是結構規則中便不需要有交換規則。G1_{cp}是包含合取析取蘊含的序列演算的邏輯系統，可以證明它在CPC中是可靠完備的，即其中可證的定理在CPC中都是有效式。類似的對于G1_{ip}在直覺主義邏輯中也是可靠完備的。直覺主義序列演算要求序列的右邊Δ集合至多含有一個公式。教授随即舉出了G1_{cp}中可證的公式          并指出它在G1_{ip}中并不可證。

在講座的第二部分，Lemhoff教授主要介紹了多種邏輯系統下的序列演算和一些重要定理。首先Lemhoff教授引入模态邏輯的概念，即在邏輯形式語言中引入模态操作符Œ。模态邏輯符在哲學、計算機、數學等領域都是一個重要的研究對象。Lemhoff教授重點讨論了G1和G3系統，它們的區别在于G3沒有結構規則但是擴展了它的公理達到與G1+Cut的等價性。Cut規則是符合人們通常數學證明直觀的規則，即通過證明引理來證明目标定理。因為結構規則和Cut規則的存在使得G1不像G3一樣擁有一些很好的性質，比如演繹的子公式特征、證明檢索的可終止性。于是我們很自然地想到消去Cut的使用，教授說明了消去Cut規則會使得證明的體量顯著增大。

第三部分是序列演算的存在性。Lemhoff教授的報告十分詳盡，她介紹了存在性的起源發展和當今研究現狀，也介紹了許多積極的研究成果。雖然我們可以對所有邏輯系統定義出它的序列演算，但并不具有良好的、像G3那樣的、可用于計算的性質。于是Lemhoff教授參照G3給出了一個序列演算是良好的定義。之後Lemhoff教授進一步闡述了良好序列演算的概念并在一些邏輯系統中讨論該良好序列演算的存在性。比如模态邏輯、中間邏輯、條件邏輯等都具備良好的序列演算。但證明一個邏輯系統不具備良好的序列演算并不是一個平凡的過程。我們采取的通用方法是對于一個邏輯類找到其中一個良好演算的必要性質P，在證明其一個子類不具備該性質從而證明該子類不具備良好演算。但P的選取并非一個容易的過程，選取過強或過弱都會帶來一些困難。Lemhoff以中間邏輯為例，選取的性質P是一緻插值UIP并給出了證明該性質的方法。此處插值是指對于一個演繹           可以找到一個公式            使得         且

。通過一緻插值性質可以證明中間邏輯中僅有7個邏輯具有良好的演算，即IPC,Sm,Gsc,LC,KC,Bd2,CPC，而例如S4,K4系統并沒有這樣的性質，即使它們存在一些很好的演算但并沒有達到我們需要的計算标準。

在評論環節，首先由林哲副教授進行簡短的評論，并提問如果不是限制在G4中而是更為自由的序列演算如标号演算以上的結果是否仍然成立。Lemhoff教授指出所介紹的方法是通用的，但在例如标号演算中證明UIP性質可能會變得比較困難。接着林哲副教授指出除了UIP之外的性質，比如cut-elimination等會依賴于演算的形式所以良好演繹的記号會發生變化。程勇教授接着提問UIP是否是良好演算的充分條件，Lemhoff教授認為可能并非如此，這是一個值得研究并且她正在研究的問題。學術志參會者和會議其他參會者也與Lemhoff進行了詳細深刻的交流。

最後，程勇教授對本場講座進行了總結，并對Lemhoff教授帶來的精彩講座表示了感謝。

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