Sequent

In proof theory, a sequent is a formalized statement of provability that is frequently used when specifying calculi for deduction. A sequent has the form

Γ |- Σ

where both Γ and Σ are sequences of logical formulae (i.e. both the number and the order of the occuring formulae matter). The symbol |- is usually referred to as turnstile, or, more suggestively, read as "proves". Γ is called the antecedent and Σ is said to be the succedent of the sequent.

The intuitive meaning of a statement as the one given above is that under the assumption of Γ the conclusion of Σ is provable. In a classical setting, the formulae on the left of the turnstile are interpreted conjunctively while the formulae on the right are considered as a disjunction. This means that, when all formulae in Γ hold, then at least one formula in Σ also has to be true. If the succedent is empty, this is interpreted as falsity, i.e. Γ |- means that Γ proves falsity and is thus inconsistent. On the other hand an empty antecedent is assumed to be true, i.e. |- &Sigma means that Σ follows without any assumptions, i.e. it is always true (as a disjunction).

The above interpretation, however, is only pedagogical. Since formal proofs in proof theory are purely syntactically, the meaning of (the derivation of) a sequent is only given by the properties of the calculus that provides the actual rules of inference.

The general notion of sequent introduced here can be specialized in various ways. A sequent is said to be an intuitionistic sequent if there is at most one formula in the succedent. This form is needed to obtain calculi for intuitionistic logic.

In many cases, sequents are also assumed to consist of multisets[?] or sets instead of sequences. Thus one disregards the order or even the number of occurences of the formulae. For classical propositional logic this does not yield a problem, since the conclusions that one can draw from a collection of premisses does not depend on these data. In substructural logic[?], however, this may become quite important.

Historically, sequents have been introduced by Gentzen in order to specify his famous sequent calculus. In his German publication he used the word "Sequenz". However, in English, the word "sequence" in already used as a translation to the German "Folge" and appears quite frequently in mathematics. The term "sequent" then has been created in search for an alternative translation of the German expression.