解释

相继式有如下形式

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

直觉意义

上面给出的那种相继式的直觉意义是在假定了Γ推出Σ是可证明的之下的。在经典的情形下，在十字转门左面的公式按合取解释，而右面的公式按析取解释。这意味着当在Γ中的所有公式成立的时候，在Σ中至少有一个公式必定是真的。如果后继为空，则按虚假解释，就是说意味着Γ证明了虚假，并且因此是矛盾的。在另一方面，空前件被假定为真，就是说意味着Σ没有任何假定就成立，也就是说，它总是真（作为一个析取式），而且因此是一个断言。

但是上述解释只用于教学目的。因为在证明论中的形式证明是纯粹的语法上的，相继式的语义只由提供实际的推理规则的演算的性质给出。

剥离在上面的技术性精确定义中的任何矛盾，我们可以按它们的介绍性的逻辑形式来描述相继式。表示我们开始逻辑处理时做的假定的集合，例如"苏格拉底是人"和"所有人都是必死的"。表示从这些前提得到的逻辑结论。例如，我们希望在十字转门的端见到"苏格拉底是必死的"。在这个意义上，意味着推理过程，或者英语中的"所以"。

我们对这些符号指派的意思是有所助益的。规则自身按机械性本质来运做而不承载潜在的意义。这个主题的详情请参见哥德尔不完备定理。

例子

一个典型的相继式：

它声称要么要么可以推导自且。

性质

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

规则

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

一个典型的规则是：