相继式演算

在证明论和数理逻辑中，相继式演算（又译矢列演算、矢列式演算、序贯演算）是一阶逻辑（和作为它的特殊情况的命题逻辑）、模态逻辑等逻辑的一类证明演算（英语：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]