相继式演算式可证明的形式陈述。是一阶逻辑的演绎系统。

「LK系统」「Gentzen系统」

相继式的一般形式为Γ⊢Σ\Gamma\vdash\Sigma
⊢\vdash被称作十字转门，读作“产生”或“证明”，Γ\Gamma叫做相继式的前件，Σ\Sigma叫做相继式的后继。
相继式的LHS（左手端）是合取，RHS（右手端）是析取。当LHS为空，此相继式是重言式。

因为在（左边的）的前件中的所有公式都必须为真来获得在（右边的）后继中至少一个公式为真，向任何一端增加公式都导致一个更弱的相继式，而从任何一端去除公式都得到更强的相继式。

多数证明系统都提供从一个相继式到另一个相继式的演绎方式。这些规则都写成在横线上下的相继式列表。这些规则指示如果在横线上的所有相继式都为真，则在横线之下的也都为真。

一个典型的规则是：

Γ⊢ΣΓ,α⊢Σα,Γ⊢Σ{\Gamma\vdash\Sigma} \over {\begin{matrix} \Gamma,\alpha\vdash\Sigma & \alpha,\Gamma\vdash\Sigma \end{matrix}}

这指示了如果我们可以演绎Σ\Sigma自Γ\Gamma，则我们也可以演绎它自Γ\Gamma和α\alpha一起。

注意我们通常使用大写的希腊字母来指称（可能为空）公式的列表。[Γ,Σ][\Gamma,\Sigma]被用来指示Γ\Gamma和Σ\Sigma的紧缩，就是说，这些出现在要么Γ\Gamma要么Σ\Sigma中但不重复的那些公式的列表。