在證明論和數理邏輯中,相繼式演算(又譯矢列演算、矢列式演算、序貫演算)是一階邏輯(和作為它的特殊情況的命題邏輯)、模態邏輯等邏輯的一類證明演算。第一個相繼式演算和由格哈德·根岑(Gerhard Gentzen)在1934年/1935年引入[1],作為研究自然演繹的工具;它的名字得來自德語的「Logischer Kalkül」,意思是「邏輯演算」。相繼式演算系統有時被稱為Gentzen系統[2][3][4][5],但使用時應避免與同為Gentzen發明的證明演算自然演繹混淆。自然演繹、公理系統和相繼式演算是常見的證明演算。
相繼式演算是邏輯研究的重要工具。許多邏輯學者會為其所研究的邏輯構造出一個或多個相繼式演算,並研究其性質(如切消定理)[6][7]。
分類不同風格的演繹系統的一種方式是查看在系統中「判斷」的形式,就是說,什麼事物可以作為(子)證明的結論出現。最簡單的判斷形式是用在希爾伯特演繹系統中的,這裡的判斷有形式
這個是一階邏輯的任何公式(或演繹系統適用的任何邏輯,比如命題演算或高階邏輯或模態邏輯)。定理出現為有效證明中結論判斷。希爾伯特演繹系統不需要區分公式和判斷;提及它只是為了和下面的情況做比較。
希爾伯特演繹系統的簡單語法付出的代價是完整的形式證明變得非常長。在這種系統中的關於證明的具體論證總是求助於演繹定理。這導致了把演繹定理包括為系統中的形式規則的想法,這激發出了自然演繹。在自然演繹中,判斷有形式
這裡的和是公式並且。用語言表述,判斷組成自十字轉門符號「」左手端的公式(可能為空)列表與右手端的一個單一公式[8][9][10]。定理是那些公式使得(帶有空左手端)是一個有效證明的結論。(在某些自然演繹的介紹中,和十字轉門是不明顯寫出來的,轉而使用二維表示法)。
在自然演繹中判斷的標準語義是斷言只要[11] , 等都是真的,就也是真的。判斷
- 與
是在任何一個的證明都可以擴展為另一個的證明的強烈意義上等價的。
最後,「相繼式演算」推廣了自然演繹的形式為
- ,
這個語法對象叫做相繼式[12]。再次和是公式,而和是非負整數,就是說左手端或右手端都可以為空或不空。如同自然演繹,定理是那些這裡的是有效證明的結論。
相繼式的標準語義是斷言只要都是真的,「至少一個」也是真的[13]。表達這個的一種方式是在十字轉門左側的逗號要被認為是「合取」,而在十字轉門右側的逗號要被認為是(包容性的)「析取」。相繼式
- 與
是在任何一個的證明都可以擴展為另一個的證明的強烈意義上等價的。
在第一印象上,這種判斷的擴展可能帶來奇怪的複雜性—它不是由於自然演繹的有明顯缺陷而激發來的,人們最初被逗號在十字轉門的兩側完全意味着不同的事物搞糊塗了。但是觀察到相繼式的語義還可以(通過命題重言式)被表達為
在這種公式中,在十字轉門兩側的公式間的唯一不同是在左側的公式被否定了。因為對換相繼式左右側的公式對應於否定所有構成公式。這意味着對稱性,如邏輯否定的德·摩根定律在語義層次上所顯現的,直接轉換到了相繼式的左右對稱—實際上,在相繼式中處理合取()、的推理規則處理析取()的推理規則的鏡像。
很多邏輯學家覺得這種對應的對稱表述允許提供比其他證明系統在邏輯結構上的深刻洞察,這裡的否定的對偶性不出現在規則中。
在這個演算中的(形式)證明是一序列的相繼式,這個的每個相繼式使用下面的推理規則之一而推導自更早出現的相繼式。
將要使用下列符號:
- 和指示一階謂詞邏輯的公式(你也可以把它限制為命題邏輯),
- 、、和是有限的(可能為空)公式序列,也叫做上下文,
- 指示一個任意的項,
- 指示一個公式,在其中項的某個出現是我們感興趣的
- 指示把在中的的指定出現代換為項,
- 和指示變量,
- 一個變量被稱為在一個公式中自由出現,如果它只出現於不在量詞或作用域內的公式中,
- 和表示弱化左/右,和表示緊縮左/右,而和表示排列左/右。
公理: |
切:
|
|
|
左邏輯規則: |
右邏輯規則:
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
限制:在規則和中,變量一定不能在或中自由出現。
左結構規則: |
右結構規則:
|
|
|
|
|
|
|
作為一個例子,下面是叫做排中律(拉丁語tertium non datur)的的序列推導。
這個推導還強調了語法演算的嚴格形式結構。例如,上述定義的右邏輯規則總是作用於右相繼式的第一個公式,這使得的應用在形式上是需要的。這種非常嚴格的推理開始時可能難於理解,但是它形成了在形式邏輯中語法和語義之間非常核心的區別。儘管我們知道和有相同的意義,對後者的推導將不等價於上面給出的那個。但是,你可以通過介入引理而使語法推理更加方便些,就是說,預定義完成特定標準推導的方案。作為一個例子,你可以證明下列是一個合法的變換:
一旦已知一個一般的規則序列要建立這種推導,你可以使用它作為證明內的縮寫。但是,當證明使用了好的引理而變得更加易讀的時候,也使得推導的過程更加複雜,因為有更多可能的選擇要考慮。在使用證明論(經常需要)作為自動演繹的時候這特別重要。
這個規則系統可以被證明關於一階邏輯是可靠的和完備的,就是說,從前提的集合Γ語義上得到的一個陳述,當且僅當相繼式可以用上述規則推導出來。
在相繼式演算中,切是可接納的。這個結果也稱為Gentzen的Hauptsatz("主定理")。
人們可以限制或禁用某個結構規則。這產生了亞結構邏輯系統變體。它們一般要弱於(就是說有更少的定理),因為關於標準的一階邏輯語義是不完備的。但是它們的其他有趣性質導致其在理論計算機科學和人工智能中的應用。
Curry 1977,第189–244頁, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.
Kleene 2009,第440–516頁. This book is much more concerned with the theoretical, metamathematical implications of Gentzen-style sequent calculus than applications to practical logic proofs.
Kleene 2002,第283–312, 331–361頁, defines Gentzen systems and proves various theorems within these systems, including Gödel's completeness theorem and Gentzen's theorem.
Curry 1977,第208–213頁, gives a 5-page proof of the elimination theorem. See also pages 188, 250.
Kleene 2009,第453頁, gives a very brief proof of the cut-elimination theorem.
Curry 1977,第184–244頁, compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical.
Suppes 1999,第25–150頁, is an introductory presentation of practical natural deduction of this kind. This became the basis of System L.
Lemmon 1965 is an elementary introduction to practical natural deduction based on the convenient abbreviated proof layout style System L based on Suppes 1999,第25–150頁.
這裡的「只要」是如下的非正式略寫「對值到判斷中的自由變量的所有指派」。
- Buss, Samuel R. An introduction to proof theory. Samuel R. Buss (編). Handbook of proof theory. Elsevier. 1998: 1–78 [2022-04-20]. ISBN 0-444-89840-9. (原始內容存檔於2021-05-17).
- Curry, Haskell Brooks. Foundations of mathematical logic. New York: Dover Publications Inc. 1977 [1963]. ISBN 978-0-486-63462-3.
- Gentzen, Gerhard Karl Erich. Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift. 1934, 39 (2): 176–210 [2022-04-20]. S2CID 121546341. doi:10.1007/BF01201353. (原始內容存檔於2020-03-07).
- Gentzen, Gerhard Karl Erich. Untersuchungen über das logische Schließen. II. Mathematische Zeitschrift. 1935, 39 (3): 405–431. S2CID 186239837. doi:10.1007/bf01201363.
- Girard, Jean-Yves; Paul Taylor; Yves Lafont. Proofs and Types. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7). 1990 [1989]. ISBN 0-521-37181-3.
- Hilbert, David; Bernays, Paul. Grundlagen der Mathematik II Second. Berlin, New York: Springer-Verlag. 1970 [1939]. ISBN 978-3-642-86897-9.
- Kleene, Stephen Cole. Introduction to metamathematics. Ishi Press International. 2009 [1952]. ISBN 978-0-923891-57-2.
- Kleene, Stephen Cole. Mathematical logic. Mineola, New York: Dover Publications. 2002 [1967]. ISBN 978-0-486-42533-7.
- Lemmon, Edward John. Beginning logic. Thomas Nelson. 1965. ISBN 0-17-712040-1.
- Smullyan, Raymond Merrill. First-order logic. New York: Dover Publications. 1995 [1968]. ISBN 978-0-486-68370-6.
- Suppes, Patrick Colonel. Introduction to logic. Mineola, New York: Dover Publications. 1999 [1957]. ISBN 978-0-486-40687-9.