相繼式演算

在證明論和數理邏輯中，相繼式演算在1934年/1935年引入，作為研究自然演繹的工具；它的名字得來自德語的“Logischer Kalkül”，意思是“邏輯演算”。相繼式演算系統有時被稱為Gentzen系統，但使用時應避免與同為Gentzen發明的證明演算自然演繹混淆。自然演繹、公理系統和相繼式演算是常見的證明演算。相繼式演算是邏輯研究的重要工具。許多邏輯學者會為其所研究的邏輯構造出一個或多個相繼式演算，並研究其性質。介紹.分類不同風格的演繹系統的一種方式是檢視在系統中“判斷”的形式，就是說，什麼事物可以作為證明的結論出現。最簡單的判斷形式是用在希爾伯特演繹系統中的，這裡的判斷有形式formula_3這個formula_3是一階邏輯的任何公式。定理出現為有效證明中結論判斷。希爾伯特演繹系統不需要區分公式和判斷；提及它只是為了和下面的情況做比較。希爾伯特演繹系統的簡單語法付出的代價是完整的形式證明變得非常長。在這種系統中的關於證明的具體論證總是求助於演繹定理。這導致了把演繹定理包括為系統中的形式規則的想法，這激發出了自然演繹。在自然演繹中，判斷有形式formula_5這裡的formula_6和formula_3是公式並且formula_8。用語言表述，判斷組成自十字轉門符號“formula_9”左手端的公式。在自然演繹中判斷的標準語義是斷言只要 formula_13, formula_14等都是真的，formula_3就也是真的。判斷formula_16與formula_17是在任何一個的證明都可以擴充套件為另一個的證明的強烈意義上等價的。最後，“相繼式演算”推廣了自然演繹的形式為formula_18，這個語法物件叫做相繼式。再次formula_6和formula_20是公式，而formula_21和formula_22是非負整數，就是說左手端或右手端都可以為空或不空。如同自然演繹，定理是那些formula_3這裡的formula_11是有效證明的結論。相繼式的標準語義是斷言只要formula_6都是真的，“至少一個”formula_20也是真的。表達這個的一種方式是在十字轉門左側的逗號要被認為是“合取”，而在十字轉門右側的逗號要被認為是“析取”。相繼式formula_27與formula_28是在任何一個的證明都可以擴充套件為另一個的證明的強烈意義上等價的。在第一印象上，這種判斷的擴充套件可能帶來奇怪的複雜性—它不是由於自然演繹的有明顯缺陷而激發來的，人們最初被逗號在十字轉門的兩側完全意味著不同的事物搞糊塗了。但是觀察到相繼式的語義還可以被表達為formula_29在這種公式中，在十字轉門兩側的公式間的唯一不同是在左側的公式被否定了。因為對換相繼式左右側的公式對應於否定所有構成公式。這意味著對稱性，如邏輯否定的德·摩根定律在語義層次上所顯現的，直接轉換到了相繼式的左右對稱—實際上，在相繼式中處理合取的推理規則的映象。很多邏輯學家覺得這種對應的對稱表述允許提供比其他證明系統在邏輯結構上的深刻洞察，這裡的否定的對偶性不出現在規則中。LK系統.在這個演算中的證明是一序列的相繼式，這個的每個相繼式使用下面的推理規則之一而推導自更早出現的相繼式。推理規則.將要使用下列符號：限制：在規則formula_56和formula_57中，變數formula_47一定不能在formula_59或formula_35中自由出現。直覺解釋.上面的規則可以被分成兩個主要群組：邏輯規則和結構規則。每個邏輯規則都在十字轉門formula_9的左邊或右邊介入一個新的邏輯公式。相反的，結構規則操作在相繼式的結構上，忽略公式的準確形狀。這個一般模式的兩個例外是同一性公理formula_62和規則切formula_63。儘管是以形式方式陳述的，上述規則允許用經典邏輯的方式非常直覺的讀出來。比如，考慮規則formula_64。它陳述瞭如果你能證明formula_35可以從包含formula_32的公式序列推匯出來，則你也能證明formula_35自更強的假定，也就是formula_68成立。類似的，規則formula_69陳述瞭如果formula_34和formula_32足夠推匯出formula_35，則從單獨的formula_34你可以要麼仍然推匯出formula_35要麼formula_32必然為假，就是說formula_76成立。所有規則都可以用這種方式來解釋。對於量詞規則的直覺解釋，考慮規則formula_56。當然只從formula_78為真的事實推匯出formula_79成立一般是不可能的。但是如果變數formula_47在其他地方沒有被提及，則你可以假定，formula_78對formula_47的任何值都成立。其他規則應當是非常直接的。不再把規則看作是對在謂詞邏輯中合法的推導的描述，你還可以把它們當作為給定陳述構造一個證明的指導。在這種情況下規則可以自底向上的讀。例如，formula_83聲稱要證明formula_68推導自假定formula_34和formula_36，分別證明formula_32可以推導自formula_34和formula_3可以推導自formula_36就足夠了。注意，給頂某個前件，如何分解成formula_34和formula_36是不明確的。但是，只有有限多的可能需要檢查，因為前件被假定為是有限的。這也展示了證明論如何被看作是以組合方式在證明的操作：給定對formula_32和formula_3二者的證明，你可以構造一個對formula_68的證明。在查詢某個證明的時候，多數規則提供或多或少的如何做的處方。切規則是不同的：它聲稱，在公式formula_32可以被推匯出來，並且這個公式也可以充當推導其他公式的前提的時候，則公式formula_32可以被"切掉"並把各自的推導連線起來。在自底向上構造一個證明的時候，這產生了猜測formula_32的問題。這個問題在切消定理中處理。第二個規則有某種特殊性，它就是同一性公理formula_62。明顯的直覺讀為：formula_32證明formula_32。例子推導.作為一個例子，下面是叫做排中律的formula_102的序列推導。formula_103這個推導還強調了語法演算的嚴格形式結構。例如，上述定義的右邏輯規則總是作用於右相繼式的第一個公式，這使得formula_104的應用在形式上是需要的。這種非常嚴格的推理開始時可能難於理解，但是它形成了在形式邏輯中語法和語義之間非常核心的區別。儘管我們知道formula_105和formula_106有相同的意義，對後者的推導將不等價於上面給出的那個。但是，你可以透過介入引理而使語法推理更加方便些，就是說，預定義完成特定標準推導的方案。作為一個例子，你可以證明下列是一個合法的變換：formula_107一旦已知一個一般的規則序列要建立這種推導，你可以使用它作為證明內的縮寫。但是，當證明使用了好的引理而變得更加易讀的時候，也使得推導的過程更加複雜，因為有更多可能的選擇要考慮。在使用證明論作為自動演繹的時候這特別重要。結構規則.結構規則需要某些額外的討論。規則的名字是弱化都不重要。就是說，你可以不把它當作序列而作為集合。但是使用序列的額外努力是正當的，因為部分或全部的結構規則可以被忽略。這麼做了就得到了所謂的亞結構邏輯。LK系統的性質.這個規則系統可以被證明關於一階邏輯是可靠的和完備的，就是說，從前提的集合Γ語義上得到的一個陳述formula_113，當且僅當相繼式formula_114可以用上述規則推匯出來。在相繼式演算中，切是可接納的。這個結果也稱為Gentzen的Hauptsatz。變體.上述規則可以以各種方式修改：次要結構變更.有些修改不改變formula_1系統的本質。所有這些修改都仍可以叫做formula_1系統。首先，如上面提及的，相繼式可以被看做由集合或多重集組成。在這種情況下，排列和緊縮公式的規則就可以廢棄了。弱化規則也變成是可接納的了，在公理formula_62被變更的時候，使得形如formula_118的任何相繼式都可以被得出。這意味著在任何上下文中formula_32證明formula_32。在推導中的任何弱化因此可以在開始處正確的進行。在自底向上構造證明的時候這是個方便的變更。獨立於這些修改，你還可以在規則內上下文被分割的方式：在formula_83、formula_122和formula_123的情況下，在向上走的時候，左上下文被以某種方式分割成formula_34和formula_36。因為緊縮允許它們的重複，你可以假定全部上下文在兩個推導分支中都使用。透過這麼做，你能確保沒有重要的前提在錯誤的分支中被丟失。使用弱化，上下文中無關的部分以後可以被消去。所有這些改變生成等價的系統，這是在LK中的所有推導可以有效的變換因使用了替代規則的推導反之亦然的意義上。亞結構邏輯.人們可以限制或禁用某個結構規則。這產生了亞結構邏輯系統變體。它們一般要弱於formula_1，因為關於標準的一階邏輯語義是不完備的。但是它們的其他有趣性質導致其在理論計算機科學和人工智慧中的應用。LJ系統.令人驚訝的，formula_1的規則的一些細小的變更就足以把它變成直覺邏輯的證明系統。你必須限制使用直覺相繼式並修改規則formula_122為如下：formula_129這裡的formula_109是任意的公式。結果的系統叫做formula_2系統。它關於直覺邏輯是可靠的和完備的並且容許類似的切消證明。