相继式演算

相继式演算把推理状态写成 $\mathrm{\Gamma }\Rightarrow \mathrm{\Delta }$，把“可用资源”和“目标候选”显式放在两侧。每条逻辑规则只分解一个主联结词，结构规则则管理上下文中的弱化、收缩与交换，因此证明像自顶向下消解公式复杂度，局部结构非常清晰；切规则则集中表达“使用中间引理”。

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

要证明 $P\wedge Q\Rightarrow P$，先由恒等公理得到 $P\Rightarrow P$，再用左弱化加入 $Q$ 得到 $P,Q\Rightarrow P$，最后用左合取规则得到目标。经典多后件系统允许 $\mathrm{\Delta }$ 表示析取，直觉主义系统常限制右侧至多一个公式。随意删除左侧假设对应逆弱化，并非普遍合法规则。

切消定理理路切消定理Cut-elimination theorem · Hauptsatz相继式演算中的切规则可被消去，从而得到只使用子公式的证明。说明切规则虽方便却非证明力所必需，并导出子公式性质与一致性结果。作为 形式系统理路形式系统Formal system · Formal calculus由符号、形成规则、公理与推导规则组成的精确定义系统。，相继式演算与相应逻辑的自然演绎理路自然演绎Natural deduction用引入规则与消去规则直接刻画逻辑联结词推理行为的证明演算。可互译。自然演绎侧重联结词的引入、消去和临时假设的解除；相继式演算则把左右上下文及其结构规则直接写进判断。互译保留的是可证明的结论，不表示两边原本使用同一种证明对象。相继式演算是证明搜索、自动定理证明和证明复杂度的标准框架，也为线性逻辑、显示逻辑和结构证明论提供可改造的骨架。