In approaches to proof theory known as sequent calculi, a pair of two multisets or sequences of formulae $\text{Γ}$ and $\Delta$, represented as:

A sequent calculus proceeds by deriving sequents from earlier sequents by means of rules. The antecedent $\text{Γ}$ is read conjunctively while the succedent is read disjunctively. In many deductive systems (such as classical logic), a sequent $\text{Γ}\Rightarrow \Delta$ is derivable in the sequent calculus if and only if the formula $\bigwedge \text{Γ}\to \bigvee \Delta$ is a theorem of that logic. Restrictions on the type of cedents employed in a logic’s sequent calculus can correspond to subsystems of that logic. For example, the sequent calculus for intuitionistic logic ($\text{LJ}$ ) is distinct from the calculus for classical logic ($\text{LK}$) by restricting the size of the succedent $\Delta$ to at most one member.