相继式演算

相继式演算把推理状态写成 $\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,Q\Rightarrow P$，再由恒等公理结束。经典多后件系统允许 $\mathrm{\Delta }$ 表示析取，直觉主义系统常限制右侧至多一个公式。随意删除左侧假设对应逆弱化，并非普遍合法规则。

切消定理公理库切消定理Cut-elimination theorem · Hauptsatz相继式演算中的切规则可被消去，从而得到只使用子公式的证明。说明切规则虽方便却非证明力所必需，并导出子公式性质与一致性结果。作为 形式系统公理库形式系统Formal system · Formal calculus由符号、形成规则、公理与推导规则组成的精确定义系统。，相继式演算与 自然演绎公理库自然演绎Natural deduction用引入规则与消去规则直接刻画逻辑联结词推理行为的证明演算。可互译，是证明搜索、自动定理证明和证明复杂度的标准框架，也为线性逻辑、显示逻辑和结构证明论提供可改造的骨架。