Sequent (in logic)
An expression of the form
where $A_1,\ldots,A_n,B_1,\ldots,B_m$ are formulas. It is read as follows. Under the assumptions $A_1,\ldots,A_n$, at least one of $B_1,\ldots,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\&\ldots\&A_n)\supseteq(B_1\lor\ldots\lor B_m)$ (note that an empty conjunction denotes truth, and an empty disjunction denotes falsity) is called the formula image of the sequent.
Some authors (particularly those working in the context of constructive logic) restrict the term "sequent" to mean an expression of the form
i.e. the particular case $m=1$ of the above definition.
|[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|
Sequent (in logic). Encyclopedia of Mathematics. URL: http://www.encyclopediaofmath.org/index.php?title=Sequent_(in_logic)&oldid=32490