相继式演算

在证明论和数理逻辑中，相继式演算（又译矢列演算、矢列式演算、序贯演算）是一阶逻辑（和作为它的特殊情况的命题逻辑）、模态逻辑等逻辑的一类证明演算（英语：Proof_calculus）。第一个相继式演算${\displaystyle LK}$和${\displaystyle LJ}$由格哈德·根岑（Gerhard Gentzen）在1934年/1935年引入，作为研究自然演绎的工具；它的名字得来自德语的“Logischer Kalkül”，意思是“逻辑演算”。相继式演算系统有时被称为Gentzen系统，但使用时应避免与同为Gentzen发明的证明演算自然演绎混淆。自然演绎、公理系统和相继式演算是常见的证明演算。

相继式演算是逻辑研究的重要工具。许多逻辑学者会为其所研究的逻辑构造出一个或多个相继式演算，并研究其性质（如切消定理）。

分类不同风格的演绎系统的一种方式是查看在系统中“判断”的形式，就是说，什么事物可以作为（子）证明的结论出现。最简单的判断形式是用在希尔伯特演绎系统中的，这里的判断有形式

这个${\displaystyle B}$是一阶逻辑的任何公式（或演绎系统适用的任何逻辑，比如命题演算或高阶逻辑或模态逻辑）。定理出现为有效证明中结论判断。希尔伯特演绎系统不需要区分公式和判断；提及它只是为了和下面的情况做比较。

希尔伯特演绎系统的简单语法付出的代价是完整的形式证明变得非常长。在这种系统中的关于证明的具体论证总是求助于演绎定理。这导致了把演绎定理包括为系统中的形式规则的想法，这激发出了自然演绎。在自然演绎中，判断有形式

这里的${\displaystyle A_i}$和${\displaystyle B}$是公式并且${\displaystyle n\ge <!--\; \ge \; -->0}$。用语言表述，判断组成自十字转门符号“${\displaystyle ⊢<!--\; ⊢\; -->}$”左手端的公式（可能为空）列表与右手端的一个单一公式。定理是那些公式${\displaystyle B}$使得${\displaystyle ⊢<!--\; ⊢\; -->B}$（带有空左手端）是一个有效证明的结论。（在某些自然演绎的介绍中，${\displaystyle A_i}$和十字转门是不明显写出来的，转而使用二维表示法）。

在自然演绎中判断的标准语义是断言只要 ${\displaystyle A_1}$, ${\displaystyle A_2}$等都是真的，${\displaystyle B}$就也是真的。判断

是在任何一个的证明都可以扩展为另一个的证明的强烈意义上等价的。

最后，“相继式演算”推广了自然演绎的形式为

这个语法对象叫做相继式。再次${\displaystyle A_i}$和${\displaystyle B_i}$是公式，而${\displaystyle n}$和${\displaystyle k}$是非负整数，就是说左手端或右手端都可以为空或不空。如同自然演绎，定理是那些${\displaystyle B}$这里的${\displaystyle ⊢<!--\; ⊢\; -->B}$是有效证明的结论。

相继式的标准语义是断言只要${\displaystyle A_i}$都是真的，“至少一个”${\displaystyle B_i}$也是真的。表达这个的一种方式是在十字转门左侧的逗号要被认为是“合取”，而在十字转门右侧的逗号要被认为是（包容性的）“析取”。相继式

是在任何一个的证明都可以扩展为另一个的证明的强烈意义上等价的。

在第一印象上，这种判断的扩展可能带来奇怪的复杂性—它不是由于自然演绎的有明显缺陷而激发来的，人们最初被逗号在十字转门的两侧完全意味着不同的事物搞糊涂了。但是观察到相继式的语义还可以（通过命题重言式）被表达为

在这种公式中，在十字转门两侧的公式间的唯一不同是在左侧的公式被否定了。因为对换相继式左右侧的公式对应于否定所有构成公式。这意味着对称性，如逻辑否定的德·摩根定律在语义层次上所显现的，直接转换到了相继式的左右对称—实际上，在相继式中处理合取（${\displaystyle \wedge <!--\; \wedge \; -->}$）、的推理规则处理析取（${\displaystyle \vee <!--\; \vee \; -->}$）的推理规则的镜像。

很多逻辑学家觉得这种对应的对称表述允许提供比其他证明系统在逻辑结构上的深刻洞察，这里的否定的对偶性不出现在规则中。

在这个演算中的（形式）证明是一序列的相继式，这个的每个相继式使用下面的推理规则之一而推导自更早出现的相继式。

将要使用下列符号：

${\displaystyle \frac{}{A⊢<!--\; ⊢\; -->A}(I)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->A,\mathrm{\Delta <!--\; \Delta \; -->}\mathrm{\Sigma <!--\; \Sigma \; -->},A⊢<!--\; ⊢\; -->\mathrm{\Pi <!--\; \Pi \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->},\mathrm{\Sigma <!--\; \Sigma \; -->}⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->},\mathrm{\Pi <!--\; \Pi \; -->}}(\mathit{C}\mathit{u}\mathit{t})}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->},A⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->},A\wedge <!--\; \wedge \; -->B⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}(\wedge <!--\; \wedge \; -->L_1)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->A,\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->A\vee <!--\; \vee \; -->B,\mathrm{\Delta <!--\; \Delta \; -->}}(\vee <!--\; \vee \; -->R_1)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->},B⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->},A\wedge <!--\; \wedge \; -->B⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}(\wedge <!--\; \wedge \; -->L_2)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->B,\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->A\vee <!--\; \vee \; -->B,\mathrm{\Delta <!--\; \Delta \; -->}}(\vee <!--\; \vee \; -->R_2)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->},A⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}\mathrm{\Sigma <!--\; \Sigma \; -->},B⊢<!--\; ⊢\; -->\mathrm{\Pi <!--\; \Pi \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->},\mathrm{\Sigma <!--\; \Sigma \; -->},A\vee <!--\; \vee \; -->B⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->},\mathrm{\Pi <!--\; \Pi \; -->}}(\vee <!--\; \vee \; -->L)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->A,\mathrm{\Delta <!--\; \Delta \; -->}\mathrm{\Sigma <!--\; \Sigma \; -->}⊢<!--\; ⊢\; -->B,\mathrm{\Pi <!--\; \Pi \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->},\mathrm{\Sigma <!--\; \Sigma \; -->}⊢<!--\; ⊢\; -->A\wedge <!--\; \wedge \; -->B,\mathrm{\Delta <!--\; \Delta \; -->},\mathrm{\Pi <!--\; \Pi \; -->}}(\wedge <!--\; \wedge \; -->R)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->A,\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->},\mathrm{\neg <!--\; \neg \; -->}A⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}(\mathrm{\neg <!--\; \neg \; -->}L)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->},A⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->\mathrm{\neg <!--\; \neg \; -->}A,\mathrm{\Delta <!--\; \Delta \; -->}}(\mathrm{\neg <!--\; \neg \; -->}R)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->A,\mathrm{\Delta <!--\; \Delta \; -->}\mathrm{\Sigma <!--\; \Sigma \; -->},B⊢<!--\; ⊢\; -->\mathrm{\Pi <!--\; \Pi \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->},\mathrm{\Sigma <!--\; \Sigma \; -->},A\to <!--\; \to \; -->B⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->},\mathrm{\Pi <!--\; \Pi \; -->}}(\to <!--\; \to \; -->L)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->},A⊢<!--\; ⊢\; -->B,\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->A\to <!--\; \to \; -->B,\mathrm{\Delta <!--\; \Delta \; -->}}(\to <!--\; \to \; -->R)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->},A⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->},\mathrm{\forall <!--\; \forall \; -->}xA⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}(\mathrm{\forall <!--\; \forall \; -->}L)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->A,\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->\mathrm{\exists <!--\; \exists \; -->}xA,\mathrm{\Delta <!--\; \Delta \; -->}}(\mathrm{\exists <!--\; \exists \; -->}R)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->},A⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->},\mathrm{\exists <!--\; \exists \; -->}xA⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}(\mathrm{\exists <!--\; \exists \; -->}L)}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->A,\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->\mathrm{\forall <!--\; \forall \; -->}xA,\mathrm{\Delta <!--\; \Delta \; -->}}(\mathrm{\forall <!--\; \forall \; -->}R)}$

限制：在规则${\displaystyle (\mathrm{\forall <!--\; \forall \; -->}R)}$和${\displaystyle (\mathrm{\exists <!--\; \exists \; -->}L)}$中，变量${\displaystyle y}$一定不能在${\displaystyle \mathrm{\Gamma <!--\; \Gamma \; -->},A}$或${\displaystyle \mathrm{\Delta <!--\; \Delta \; -->}}$中自由出现。

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->},A⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}(\mathit{W}\mathit{L})}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->A,\mathrm{\Delta <!--\; \Delta \; -->}}(\mathit{W}\mathit{R})}$

${\displaystyle \frac{\mathrm{\Gamma <!--\; \Gamma \; -->},A,A⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->},A⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}}(\mathit{C}\mathit{L})}$