Sequent Glossary
Definition
In logic as presented in most of these notes, a sequent consists of a set of formulae called its premises and a single formula called its conclusion. It represents an argument form.
Sometimes sequents are defined to have a set of conclusions in place of the single conclusion. This is commonly done for the sequent calculus rather than for natural deduction.
Sequents in some non-classical logics such as relevant logic or some fuzzy logics may have more complex structures in place of sets.
Comments
We write
X ⊢ A
to mean that the sequent with premises X and conclusion A is provable—i.e. that there exists a derivation of A from X. By slight abuse of notation, we also refer to the sequent itself as 'X ⊢ A'.
We write
X ⊨ A
to mean that the sequent with premises X and conclusion A is valid in the sense that any interpretation satisfying all formulae in X satisfies A.