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.