An approach to proof theory developed by logician Gerhard Gentzen (1909–1945) whose primary components are sequents, comprising pairs of cedents $\text{Γ}$ and $\Delta$—multisets or sequences of formulae—typically represented either as $\text{Γ}\Rightarrow \Delta$ or $\text{Γ}⊢\Delta$. A proof in a sequent calculus consists of a finite number of applications of introduction and structural rules on a number of initial sequents, so that a sequent $\text{Γ}\Rightarrow \Delta$ is provable if it may be generated from a finite number of instances of the identity axiom $\phi \Rightarrow \phi$ by the rules of the sequent calculus. Theoremhood of a formula $\phi$ in a deductive system $\text{L}$ corresponds to the sequent $\varnothing \Rightarrow \left\{\phi \right\}$ in the appropriate sequent calculus.

While natural deduction has both introduction and elimination rules, sequent calculi tend to have only introduction rules—one corresponding to the introduction of an operator in the antecedent (a left introduction rule) and one corresponding to the introduction of an operator in the succedent (a right introduction rule). This approach leads to a number of sequent calculi enjoying the subformula property that every formula that appears in a sequent in some stage of a proof ultimately appears as a subformula of some formula in the final sequent.

There are cases in which the standard Gentzen-type approach to sequent calculi falls short, such as a number of many-valued logics and modal logics. In the former case, frequently signed formulae are introduced, where each formula is tagged with a syntactic element playing the role of a truth value. In the latter case, hypersequent calculi have been employed, in which a hypersequent—a list of sequents—captures a notion of possibility by being interpreted as a set of sequents that could be valid.