View source for Sequent (in logic)

An expression of the form

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845901.png" /></td> </tr></table>

where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845902.png" /> are formulas. It is read as follows. Under the assumptions <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845903.png" />, at least one of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845904.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845905.png" /> (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

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845906.png" /></td> </tr></table>

i.e. the particular case <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845907.png" /> 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>