In mathematical logic, a sequent is a very general kind of conditional assertion.
A sequent may have any number m of condition formulas Ai (called "antecedents") and any number n of asserted formulas Bj (called "succedents" or "consequents"). A sequent is understood to mean that if all of the antecedent conditions are true, then at least one of the consequent formulas is true. This style of conditional assertion is almost always associated with the conceptual framework of sequent calculus.
Sequents are best understood in the context of the following three kinds of logical judgments:
Thus sequents are a generalization of simple conditional assertions, which are a generalization of unconditional assertions.
The word "OR" here is the inclusive OR. The motivation for disjunctive semantics on the right side of a sequent comes from three main benefits.
All three of these benefits were identified in the founding paper by Gentzen (1934, p. 194).
Not all authors have adhered to Gentzen's original meaning for the word "sequent". For example, Lemmon (1965) used the word "sequent" strictly for simple conditional assertions with one and only one consequent formula. The same single-consequent definition for a sequent is given by Huth & Ryan 2004, p. 5.
In a general sequent of the form
both Γ and Σ are sequences of logical formulas, not sets. Therefore both the number and order of occurrences of formulas are significant. In particular, the same formula may appear twice in the same sequence. The full set of sequent calculus inference rules contains rules to swap adjacent formulas on the left and on the right of the assertion symbol (and thereby arbitrarily permute the left and right sequences), and also to insert arbitrary formulas and remove duplicate copies within the left and the right sequences. (However, Smullyan (1995, pp. 107–108), uses sets of formulas in sequents instead of sequences of formulas. Consequently the three pairs of structural rules called "thinning", "contraction" and "interchange" are not required.)