在证明论中，相继式是对在规定演绎的演算的时候经常用到的可证明性的形式陈述。

相继式有如下形式

这里的Γ和Σ二者是逻辑公式的串行（就是说公式的数目和出现次序都是重要的）。符号通常被称为十字转门（turnstile）或T型符号（tee），并经常被读做"产生"或"证明"。它不是语言中的符号，而用来讨论证明的元语言中的符号。在相继式中，Γ叫做相继式的前件（antecedent）而Σ叫做相继式的后继（succedent）。

In mathematical logic, a sequent is a very general kind of conditional assertion.

A sequent may have any number m of condition formulas A_i (called "antecedents") and any number n of asserted formulas B_j (called "succedents" or "consequents"). A sequent is understood to mean that if all of the antecedent conditions are true, then at least one of the consequent formulas is true. This style of conditional assertion is almost always associated with the conceptual framework of sequent calculus.