# Dictionary Definition

sequent adj

1 in regular succession without gaps; "serial
concerts" [syn: consecutive, sequential, serial, successive]

2 following as an effect or result; "the period
of tension and consequent need for military preparedness"; "the
ensuant response to his appeal"; "the resultant savings were
considerable"; "the health of the plants and the resulting flowers"
[syn: consequent,
ensuant, resultant, resulting(a)]

# User Contributed Dictionary

## English

### Noun

- An element of a sequence, usually a sequence in which every entry is an axiom or can be inferred from previous elements

# Extensive Definition

In proof
theory, a sequent is a formalized statement of provability that
is frequently used when specifying calculi
for deduction.
In the sequent
calculus, the name sequent is used for the construct which can
be regarded as a specific kind of
judgment, characteristic to this deduction system.

## Explanation

A sequent has the form

- \Gamma\vdash\Sigma

where both Γ and Σ are
sequences of logical
formulae (i.e., both the number and the order of the occurring
formulae matter). The symbol \vdash is usually referred to as
turnstile or tee and is often read, suggestively, as "yields" or
"proves". It is not a symbol in the language, rather it is a symbol
in the metalanguage
used to discuss proofs. In a sequent, Γ is called the
antecedent and Σ is said to be the succedent of the
sequent.

## Intuitive meaning

The intuitive meaning of a sequent such 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. \Gamma\vdash means that Γ proves falsity and is thus inconsistent. On the other hand an empty antecedent is assumed to be true, i.e., \vdash\Sigma means that Σ follows without any assumptions, i.e., it is always true (as a disjunction). A sequent of this form, with Γ empty, is known as a logical assertion.The above interpretation, however, is only
pedagogical. Since formal proofs in proof theory are purely
syntactic, the meaning of (the derivation of)
a sequent is only given by the properties of the calculus that
provides the actual rules of
inference.

Barring any contradictions in the technically
precise definition above we can describe sequents in their
introductory logical form. \Gamma represents a set of assumptions
that we begin our logical process with, for example "Socrates is a
man" and "All men are mortal". The \Sigma represents a logical
conclusion that follows under these premises. For example "Socrates
is mortal" follows from a reasonable formalization of the above
points and we could expect to see it on the \Sigma side of the
turnstile. In this sense, \vdash means the process of reasoning, or
"therefore" in English.

## Example

A typical sequent might be:- \phi,\psi\vdash\alpha,\beta

This claims that either \alpha or \beta can be
derived from \phi and \psi.

## Property

Since every formula in the antecedent (the left side) must be true to conclude the truth of at least one formula in the succedent (the right side), adding formulas to either side results in a weaker sequent, while removing them from either side gives a stronger one.## Rules

Most proof systems provide ways to deduce one sequent from another. These inference rules are written with a list of sequents above and below a line. This rule indicates that if everything above the line is true, so is everything under the line.A typical rule is:

- \frac

This indicates that if we can deduce \Sigma from
\Gamma, we can also deduce it from \Gamma together with
\alpha.

Note that the capital Greek letters are usually
used to denote a (possibly empty) list of formulae. [\Gamma,\Sigma]
is used to denote the contraction of \Gamma and \Sigma, that is,
the list of those formulas appearing in either \Gamma or \Sigma but
with no repeats.

## Variations

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. Similarly, one can obtain calculi for dual-intuitionistic logic (a type of paraconsistent logic) by requiring that sequents be singular in the antecedent.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 occurrences 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.

## History

Historically, sequents have been introduced by Gerhard Gentzen in order to specify his famous sequent calculus. In his German publication he used the word "Sequenz". However, in English, the word "sequence" is 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.sequent in Italian: Sequente

sequent in Japanese: シークエント

sequent in Chinese: 相继式