Sequent (in logic)

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]