相繼式演算

在證明論和數理邏輯中，相繼式演算（又譯矢列演算、矢列式演算、序貫演算）是一階邏輯（和作為它的特殊情況的命題邏輯）、模態邏輯等邏輯的一類證明演算（英語：Proof_calculus）。第一個相繼式演算 $LK$ 和 $LJ$ 由格哈德·根岑（Gerhard Gentzen）在1934年/1935年引入^[1]，作為研究自然演繹的工具；它的名字得來自德語的「Logischer Kalkül」，意思是「邏輯演算」。相繼式演算系統有時被稱為Gentzen系統^[2]^[3]^[4]^[5]，但使用時應避免與同為Gentzen發明的證明演算自然演繹混淆。自然演繹、公理系統和相繼式演算是常見的證明演算。

相繼式演算是邏輯研究的重要工具。許多邏輯學者會為其所研究的邏輯構造出一個或多個相繼式演算，並研究其性質（如切消定理）^[6]^[7]。

介紹[編輯]

分類不同風格的演繹系統的一種方式是查看在系統中「判斷」的形式，就是說，什麼事物可以作為（子）證明的結論出現。最簡單的判斷形式是用在希爾伯特演繹系統中的，這裡的判斷有形式

B

這個 $B$ 是一階邏輯的任何公式（或演繹系統適用的任何邏輯，比如命題演算或高階邏輯或模態邏輯）。定理出現為有效證明中結論判斷。希爾伯特演繹系統不需要區分公式和判斷；提及它只是為了和下面的情況做比較。

希爾伯特演繹系統的簡單語法付出的代價是完整的形式證明變得非常長。在這種系統中的關於證明的具體論證總是求助於演繹定理。這導致了把演繹定理包括為系統中的形式規則的想法，這激發出了自然演繹。在自然演繹中，判斷有形式

A_{1},A_{2},\ldots ,A_{n}\vdash B

這裡的 $A_{i}$ 和 $B$ 是公式並且 $n\geq 0$ 。用語言表述，判斷組成自十字轉門符號「 $\vdash$ 」左手端的公式（可能為空）列表與右手端的一個單一公式^[8]^[9]^[10]。定理是那些公式 $B$ 使得 $\vdash B$ （帶有空左手端）是一個有效證明的結論。（在某些自然演繹的介紹中， $A_{i}$ 和十字轉門是不明顯寫出來的，轉而使用二維表示法）。

在自然演繹中判斷的標準語義是斷言只要^[11] $A_{1}$ , $A_{2}$ 等都是真的， $B$ 就也是真的。判斷

A_{1},\ldots ,A_{n}\vdash B\quad

與

\quad \vdash (A_{1}\land \cdots \land A_{n})\rightarrow B

是在任何一個的證明都可以擴展為另一個的證明的強烈意義上等價的。

最後，「相繼式演算」推廣了自然演繹的形式為

A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k}

，

這個語法對象叫做相繼式^[12]。再次 $A_{i}$ 和 $B_{i}$ 是公式，而 $n$ 和 $k$ 是非負整數，就是說左手端或右手端都可以為空或不空。如同自然演繹，定理是那些 $B$ 這裡的 $\vdash B$ 是有效證明的結論。

相繼式的標準語義是斷言只要 $A_{i}$ 都是真的，「至少一個」 $B_{i}$ 也是真的^[13]。表達這個的一種方式是在十字轉門左側的逗號要被認為是「合取」，而在十字轉門右側的逗號要被認為是（包容性的）「析取」。相繼式

A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k}\quad

與

\quad \vdash (A_{1}\land \cdots \land A_{n})\rightarrow (B_{1}\lor \cdots \lor B_{k})

是在任何一個的證明都可以擴展為另一個的證明的強烈意義上等價的。

在第一印象上，這種判斷的擴展可能帶來奇怪的複雜性—它不是由於自然演繹的有明顯缺陷而激發來的，人們最初被逗號在十字轉門的兩側完全意味着不同的事物搞糊塗了。但是觀察到相繼式的語義還可以（通過命題重言式）被表達為

\neg A_{1}\lor \neg A_{2}\lor \cdots \neg A_{n}\lor B_{1}\lor B_{2}\lor \cdots \lor B_{k}

在這種公式中，在十字轉門兩側的公式間的唯一不同是在左側的公式被否定了。因為對換相繼式左右側的公式對應於否定所有構成公式。這意味着對稱性，如邏輯否定的德·摩根定律在語義層次上所顯現的，直接轉換到了相繼式的左右對稱—實際上，在相繼式中處理合取（ $\land$ ）、的推理規則處理析取（ $\lor$ ）的推理規則的鏡像。

很多邏輯學家覺得這種對應的對稱表述允許提供比其他證明系統在邏輯結構上的深刻洞察，這裡的否定的對偶性不出現在規則中。

LK系統[編輯]

在這個演算中的（形式）證明是一序列的相繼式，這個的每個相繼式使用下面的推理規則之一而推導自更早出現的相繼式。

推理規則[編輯]

將要使用下列符號：

$A$ 和 $B$ 指示一階謂詞邏輯的公式（你也可以把它限制為命題邏輯），
$\Gamma$ 、 $\Delta$ 、 $\Sigma$ 和 $\Pi$ 是有限的（可能為空）公式序列，也叫做上下文，
$t$ 指示一個任意的項，
$A[t]$ 指示一個公式 $A$ ，在其中項 $t$ 的某個出現是我們感興趣的
$A[s/t]$ 指示把在 $A[s]$ 中的 $s$ 的指定出現代換為項 $t$ ，
$x$ 和 $y$ 指示變量，
一個變量被稱為在一個公式中自由出現，如果它只出現於不在量詞 $\forall$ 或 $\exists$ 作用域內的公式中，
$WL$ 和 $WR$ 表示弱化左/右， $CL$ 和 $CR$ 表示緊縮左/右，而 $PL$ 和 $PR$ 表示排列左/右。

公理：	切：
${\cfrac {\qquad }{A\vdash A}}\quad (I)$	${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,A\vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})$

左邏輯規則：	右邏輯規則：
${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})$	${\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})$
${\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})$	${\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})$
${\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}\quad ({\lor }L)$	${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma \vdash B,\Pi }{\Gamma ,\Sigma \vdash A\land B,\Delta ,\Pi }}\quad ({\land }R)$
${\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)$	${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)$
${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)$	${\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)$
${\cfrac {\Gamma ,A[t]\vdash \Delta }{\Gamma ,\forall xA[x/t]\vdash \Delta }}\quad ({\forall }L)$	${\cfrac {\Gamma \vdash A[t],\Delta }{\Gamma \vdash \exists xA[x/t],\Delta }}\quad ({\exists }R)$
${\cfrac {\Gamma ,A[y]\vdash \Delta }{\Gamma ,\exists xA[x/y]\vdash \Delta }}\quad ({\exists }L)$	${\cfrac {\Gamma \vdash A[y],\Delta }{\Gamma \vdash \forall xA[x/y],\Delta }}\quad ({\forall }R)$

限制：在規則 $(\forall R)$ 和 $(\exists L)$ 中，變量 $y$ 一定不能在 $\Gamma ,A[x/y]$ 或 $\Delta$ 中自由出現。

左結構規則：	右結構規則：
${\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})$	${\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})$
${\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})$	${\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})$
${\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})$	${\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})$

直覺解釋[編輯]

上面的規則可以被分成兩個主要群組：邏輯規則和結構規則。每個邏輯規則都在十字轉門 $\vdash$ 的左邊或右邊介入一個新的邏輯公式。相反的，結構規則操作在相繼式的結構上，忽略公式的準確形狀。這個一般模式的兩個例外是同一性公理 $(I)$ 和規則切 $(Cut)$ 。

儘管是以形式方式陳述的，上述規則允許用經典邏輯的方式非常直覺的讀出來。比如，考慮規則 $\wedge L_{1}$ 。它陳述了如果你能證明 $\Delta$ 可以從包含 $A$ 的公式序列推導出來，則你也能證明 $\Delta$ 自更強的假定，也就是 $A\wedge B$ 成立。類似的，規則 $(\neg R)$ 陳述了如果 $\Gamma$ 和 $A$ 足夠推導出 $\Delta$ ，則從單獨的 $\Gamma$ 你可以要麼仍然推導出 $\Delta$ 要麼 $A$ 必然為假，就是說 $\neg A$ 成立。所有規則都可以用這種方式來解釋。

對於量詞規則的直覺解釋，考慮規則 $(\forall R)$ 。當然只從 $A[y]$ 為真的事實推導出 $\forall x,A[x/y]$ 成立一般是不可能的。但是如果變量 $y$ 在其他地方沒有被提及（就是說，它仍可以被自由的選擇，而不影響其他公式），則你可以假定， $A[y]$ 對 $y$ 的任何值都成立。其他規則應當是非常直接的。

不再把規則看作是對在謂詞邏輯中合法的推導的描述，你還可以把它們當作為給定陳述構造一個證明的指導。在這種情況下規則可以自底向上的讀。例如， $(\wedge R)$ 聲稱要證明 $A\wedge B$ 推導自假定 $\Gamma$ 和 $\Sigma$ ，分別證明 $A$ 可以推導自 $\Gamma$ 和 $B$ 可以推導自 $\Sigma$ 就足夠了。注意，給頂某個前件，如何分解成 $\Gamma$ 和 $\Sigma$ 是不明確的。但是，只有有限多的可能需要檢查，因為前件被假定為是有限的。這也展示了證明論如何被看作是以組合方式在證明的操作：給定對 $A$ 和 $B$ 二者的證明，你可以構造一個對 $A\wedge B$ 的證明。

在查找某個證明的時候，多數規則提供或多或少的如何做的處方。切規則是不同的：它聲稱，在公式 $A$ 可以被推導出來，並且這個公式也可以充當推導其他公式的前提的時候，則公式 $A$ 可以被"切掉"並把各自的推導連接起來。在自底向上構造一個證明的時候，這產生了猜測 $A$ 的問題（因為它在下面根本就沒有出現）。這個問題在切消定理中處理。

第二個規則有某種特殊性，它就是同一性公理 $(I)$ 。明顯的直覺讀為： $A$ 證明 $A$ 。

例子推導[編輯]

作為一個例子，下面是叫做排中律（拉丁語tertium non datur）的 $\vdash (A\vee \neg A)$ 的序列推導。

{\cfrac {{\cfrac {{\cfrac {{\cfrac {{\cfrac {{\cfrac {}{A\vdash A}}(I)}{\vdash \lnot A,A}}({\lnot }R)}{\vdash A\lor \lnot A,A}}({\lor }R_{2})}{\vdash A,A\lor \lnot A}}(PR)}{\vdash A\lor \lnot A,A\lor \lnot A}}({\lor }R_{1})}{\vdash A\lor \lnot A}}(CR)

這個推導還強調了語法演算的嚴格形式結構。例如，上述定義的右邏輯規則總是作用於右相繼式的第一個公式，這使得 $(PR)$ 的應用在形式上是需要的。這種非常嚴格的推理開始時可能難於理解，但是它形成了在形式邏輯中語法和語義之間非常核心的區別。儘管我們知道 $A\vee \neg A$ 和 $\neg A\vee A$ 有相同的意義，對後者的推導將不等價於上面給出的那個。但是，你可以通過介入引理而使語法推理更加方便些，就是說，預定義完成特定標準推導的方案。作為一個例子，你可以證明下列是一個合法的變換：

{\cfrac {\Gamma \vdash A\lor B,\Delta }{\Gamma \vdash B\lor A,\Delta }}

一旦已知一個一般的規則序列要建立這種推導，你可以使用它作為證明內的縮寫。但是，當證明使用了好的引理而變得更加易讀的時候，也使得推導的過程更加複雜，因為有更多可能的選擇要考慮。在使用證明論（經常需要）作為自動演繹的時候這特別重要。

結構規則[編輯]

結構規則需要某些額外的討論。規則的名字是弱化（ $W$ ）、緊縮（ $C$ ）和排列（ $P$ ）。緊縮和排列確保序列元素的次序（ $P$ ）和多次出現（ $C$ ）都不重要。就是說，你可以不把它當作序列而作為集合。

但是使用序列的額外努力是正當的，因為部分或全部的結構規則可以被忽略。這麼做了就得到了所謂的亞結構邏輯。

LK系統的性質[編輯]

這個規則系統可以被證明關於一階邏輯是可靠的和完備的，就是說，從前提的集合Γ語義上得到的一個陳述 $(\Gamma \vDash A)$ ，當且僅當相繼式 $\Gamma \vdash A$ 可以用上述規則推導出來。

在相繼式演算中，切是可接納的。這個結果也稱為Gentzen的Hauptsatz（"主定理"）。

變體[編輯]

上述規則可以以各種方式修改：

次要結構變更[編輯]

有些修改不改變 $LK$ 系統的本質。所有這些修改都仍可以叫做 $LK$ 系統。

首先，如上面提及的，相繼式可以被看做由集合或多重集組成。在這種情況下，排列和（在使用集合的時候）緊縮公式的規則就可以廢棄了。

弱化規則也變成是可接納的了，在公理 $(I)$ 被變更的時候，使得形如 $\Gamma ,A\vdash A,\Delta$ 的任何相繼式都可以被得出。這意味着在任何上下文中 $A$ 證明 $A$ 。在推導中的任何弱化因此可以在開始處正確的進行。在自底向上構造證明的時候這是個方便的變更。

獨立於這些修改，你還可以在規則內上下文被分割的方式：在 $(\wedge R)$ 、 $(\vee L)$ 和 $(\rightarrow L)$ 的情況下，在向上走的時候，左上下文被以某種方式分割成 $\Gamma$ 和 $\Sigma$ 。因為緊縮允許它們的重複，你可以假定全部上下文在兩個推導分支中都使用。通過這麼做，你能確保沒有重要的前提在錯誤的分支中被丟失。使用弱化，上下文中無關的部分以後可以被消去。

所有這些改變生成等價的系統，這是在LK中的所有推導可以有效的變換因使用了替代規則的推導反之亦然的意義上。

亞結構邏輯[編輯]

人們可以限制或禁用某個結構規則。這產生了亞結構邏輯系統變體。它們一般要弱於 $LK$ （就是說有更少的定理），因為關於標準的一階邏輯語義是不完備的。但是它們的其他有趣性質導致其在理論計算機科學和人工智能中的應用。

LJ系統[編輯]

令人驚訝的， $LK$ 的規則的一些細小的變更就足以把它變成直覺邏輯的證明系統。你必須限制使用直覺相繼式（就是說，右上下文被消去）並修改規則 $(\vee L)$ 為如下：

{\cfrac {\Gamma ,A\vdash C\qquad \Sigma ,B\vdash C}{\Gamma ,\Sigma ,A\lor B\vdash C}}\quad ({\lor }L)

這裡的 $C$ 是任意的公式。

結果的系統叫做 $LJ$ 系統。它關於直覺邏輯是可靠的和完備的並且容許類似的切消證明。

引用[編輯]

^ Gentzen 1934, Gentzen 1935.
^ 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.
^ Smullyan 1995，第101–127頁
^ 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頁.
^ 這裡的「只要」是如下的非正式略寫「對值到判斷中的自由變量的所有指派」。
^ Shankar, Natarajan; Owre, Sam; Rushby, John M.; Stringer-Calvert, David W. J. PVS Prover Guide (PDF). User guide. SRI International. 2001-11-01 [2015-05-29]. （原始內容 (PDF)存檔於2022-03-27）.
^ For explanations of the disjunctive semantics for the right side of sequents, see Curry 1977，第189–190頁, Kleene 2002，第290, 297頁, Kleene 2009，第441頁, Hilbert & Bernays 1970，第385頁, Smullyan 1995，第104–105頁 and Gentzen 1934，第180頁.

參考文獻[編輯]

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.

參見[編輯]

外部連結[編輯]

[gentzen19341935-1] Gentzen 1934, Gentzen 1935.

[2] Curry 1977，第189–244頁, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.

[3] 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.

[4] 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.

[5] Smullyan 1995，第101–127頁

[6] Curry 1977，第208–213頁, gives a 5-page proof of the elimination theorem. See also pages 188, 250.

[kleene_cut_elimination-7] Kleene 2009，第453頁, gives a very brief proof of the cut-elimination theorem.

[8] Curry 1977，第184–244頁, compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical.

[9] Suppes 1999，第25–150頁, is an introductory presentation of practical natural deduction of this kind. This became the basis of System L.

[10] 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頁.

[11] 這裡的「只要」是如下的非正式略寫「對值到判斷中的自由變量的所有指派」。

[pvs-prover-12] Shankar, Natarajan; Owre, Sam; Rushby, John M.; Stringer-Calvert, David W. J. PVS Prover Guide (PDF). User guide. SRI International. 2001-11-01 [2015-05-29]. （原始內容 (PDF)存檔於2022-03-27）.

[13] For explanations of the disjunctive semantics for the right side of sequents, see Curry 1977，第189–190頁, Kleene 2002，第290, 297頁, Kleene 2009，第441頁, Hilbert & Bernays 1970，第385頁, Smullyan 1995，第104–105頁 and Gentzen 1934，第180頁.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]