时序(Sequent)是一个表达式 
, 其中 
和 
是（可能为空的）公式序列。这里，
被称为前件(antecedent)，
被称为后件(consequent)。对时序的非正式理解是，时序 
对应于 
。所有推导的初始时序是
 |
(1)
|
时序演算的推理规则分为两类：结构规则和逻辑规则。对于每个命题连接词和每个量词，至少有两个逻辑规则；其中一个应用于前件，而另一个应用于后件。结构规则包括：弱化,
 |
(2)
|
收缩,
 |
(3)
|
交换,
 |
(4)
|
和 cut 规则,
 |
(5)
|
逻辑规则由以下规则给出：合取,
 |
(6)
|
析取,
 |
(7)
|
否定,
 |
(8)
|
蕴涵,
 |
(9)
|
全称量词,
 |
(10)
|
和存在量词
 |
(11)
|
这里，变量 
在 
中是自由的，并且 
是通过将 
中所有自由出现的 
替换为 
而获得的。在 
-后继式规则和 
-前件式规则中出现的变量 
被称为本征变量。它不得出现在相应规则的下层时序中。
时序演算指定了经典一阶逻辑，并且相同的框架也可以用于指定直觉逻辑。为了将推导限制为直觉逻辑，添加了额外的约束，即每个后继式最多只能有一个公式。根岑提出的经典（多后继式）变体称为 LK，直觉（单后继式）变体称为 LJ。LK 也可以被定义为单后继式演算，并使用排中律作为另一个基本时序进行扩充。基于时序推理规则的证明理论也称为根岑型。随后引入了许多其他基于时序的逻辑公式。
双重否定提供了一个示例推导，它在时序演算的经典变体中有效，但在直觉变体中无效。
上面显示了第二个推导（这是一个有效的直觉推导）。
时序演算是证明论的一个非常有用的工具，主要是因为 cut 规则的可容许性，它可以从推导中消除，而不会影响可推导公式的集合。
