Sequent (in logic)

An expression of the form

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

where $A_1,\dots ,A_n,B_1,\dots ,B_m$ are formulas. It is read as follows. Under the assumptions $A_1,\dots ,A_n$, at least one of $B_1,\dots ,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\mathrm{\&}\cdots \mathrm{\&}{A}_n)\supseteq (B_1\vee \cdots \vee 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,\dots ,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]