形式陈述

相继式演算以

$$ \Gamma\Rightarrow\Delta $$$$\mathrm{\Gamma }\Rightarrow \mathrm{\Delta }$$

为基本判断，其中 $\Gamma,\Delta$$\mathrm{\Gamma },\mathrm{\Delta }$ 是公式的有限序列或多重集，语义上表示 $\bigwedge\Gamma\to\bigvee\Delta$$\bigwedge \mathrm{\Gamma }\to \bigvee \mathrm{\Delta }$。规则分为结构规则（弱化、收缩、交换）、分别作用于左右两侧的逻辑规则以及切规则

$$ \frac{\Gamma\Rightarrow\Delta,A\qquad A,\Pi\Rightarrow\Lambda} {\Gamma,\Pi\Rightarrow\Delta,\Lambda}. $$$$\frac{\mathrm{\Gamma }\Rightarrow \mathrm{\Delta },AA,\mathrm{\Pi }\Rightarrow \mathrm{\Lambda }}{\mathrm{\Gamma },\mathrm{\Pi }\Rightarrow \mathrm{\Delta },\mathrm{\Lambda }}.$$

经典系统 LK 允许右侧多个公式；直觉主义系统 LJ 通常限制右侧至多一个公式。空左侧表示无前提，空右侧表示矛盾或不可达结论，具体解释随演算约定固定。

直觉

相继式把“可用资源”和“目标候选”显式放在证明状态两侧；每条逻辑规则只分解一个主公式，因此证明的局部结构非常清晰。

例子与边界

右合取规则把证明 $\Gamma\Rightarrow A\land B$$\mathrm{\Gamma }\Rightarrow A\wedge B$ 分解成分别证明 $\Gamma\Rightarrow A$$\mathrm{\Gamma }\Rightarrow A$ 与 $\Gamma\Rightarrow B$$\mathrm{\Gamma }\Rightarrow B$；左合取规则则可把假设 $A\land B$$A\wedge B$ 展开成 $A,B$$A,B$。弱化允许加入未使用假设，收缩允许合并重复假设；在线性逻辑中这些结构规则不再普遍可用，说明它们并非纯排版操作。多后承 LK 能直接表达经典析取行为，单后承 LJ 则保留构造性。把 $\Gamma,\Delta$$\mathrm{\Gamma },\mathrm{\Delta }$ 当集合会遮蔽收缩和交换是否为显式规则，因此定义时需声明上下文的数据结构。

推论与应用

相继式演算是切消、子公式性质、证明搜索与自动定理证明的标准框架，也为线性逻辑、显示逻辑和结构证明论提供可改造骨架。

参考资料

• A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, 2nd ed., Cambridge University Press, 2000，Chs. 4–6, Gentzen sequent calculi LK and LJ。
• Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas, Mathematical Logic, 2nd ed., Springer, 1994，Part A, sequent systems and structural/logical rules。