View source for Sequent (in logic)

{{TEX|done}}
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====
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|Gentzen formal system]]; [[Sequent calculus|Sequent calculus]] and, e.g., [[#References|[a2]]].

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  W. Hodges,   "Elementary predicate logic"  D. Gabbay (ed.)  F. Guenther (ed.) , ''Handbook of philosophical logic'' , '''I''' , Reidel  (1983)  pp. 1–131</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  G. Sundholm,   "Systems of deduction"  D. Gabbay (ed.)  F. Guenther (ed.) , ''Handbook of philosophical logic'' , '''I''' , Reidel  (1983)  pp. 133–188, §3</TD></TR></table>