Sequent calculus

Sequent calculi are a style of deductive system, primarily contrasted with natural deduction. Some things that differentiate sequent calculi from systems of natural deduction include:

• They have left introduction rules rather than right elimination rules.
• They usually allow multiple formulae on both the right-hand side of the turnstile (in classical systems).
• They tend to have explicit structural rules (i.e., exchange, weakening, and/or contraction) which would not be admissible if not included (there are some such systems of natural deduction, but it is much less common than in sequent calculus).
• Redexes correspond entirely to occurrences of a single rule, the cut.