An expression of the form

$$A_1,\dotsc,A_n\to B_1,\dotsc,B_m,$$

where $A_1,\dotsc,A_n,B_1,\dotsc,B_m$ are formulas. It is read as follows. Under the assumptions $A_1,\dotsc,A_n$, at least one of $B_1,\dotsc,B_m$ holds. The part of the sequent on the left of the arrow is called the antecedent, and the part on the right the succedent (consequent). The formula $(A_1\mathbin{\&}\dotsb\mathbin{\&}A_n)\supseteq(B_1\lor\dotsb\lor B_m)$ (note that an empty conjunction denotes truth, and an empty disjunction denotes falsity) is called the formula image of the sequent.

#### Comments[edit]

Some authors (particularly those working in the context of constructive logic) restrict the term "sequent" to mean an expression of the form

$$A_1,\dotsc,A_n\to B,$$

i.e. the particular case $m=1$ of the above definition.

For a discussion of Gentzen's sequent calculi cf. Gentzen formal system; Sequent calculus and, e.g., [a2].

#### References[edit]

[a1] |  W. Hodges, "Elementary predicate logic" D. Gabbay (ed.) F. Guenther (ed.) , Handbook of philosophical logic , I , Reidel (1983) pp. 1–131

|

[a2] |  G. Sundholm, "Systems of deduction" D. Gabbay (ed.) F. Guenther (ed.) , Handbook of philosophical logic , I , Reidel (1983) pp. 133–188, §3