Sequent

Sequent

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:GammavdashSigma

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. Gammavdash means that Γ proves falsity and is thus inconsistent. On the other hand an empty antecedent is assumed to be true, i.e., vdashSigma 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,psivdashalpha,eta

This claims that either alpha or eta 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{GammavdashSigma}{egin{matrix} Gamma,alphavdashSigma & alpha,GammavdashSigma end{matrix

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) set of formulae. [Gamma,Sigma] is used to denote the logical conjunction of Gamma and Sigma.

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 premises 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.


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • sequent — sequent …   New Dictionary of Synonyms

  • Sequent — Se quent, a. [L. sequens, entis, p. pr. of sequi to follow. See {Sue} to follow.] 1. Following; succeeding; in continuance. [1913 Webster] What to this was sequent Thou knowest already. Shak. [1913 Webster] 2. Following as an effect; consequent.… …   The Collaborative International Dictionary of English

  • sequent — 1550s (adj.), 1580s (n.), from O.Fr. sequent, from L. sequentem, prp. of sequi “to follow” (see SEQUEL (Cf. sequel)) …   Etymology dictionary

  • Sequent — Se quent, n. 1. A follower. [R.] Shak. [1913 Webster] 2. That which follows as a result; a sequence. [1913 Webster] …   The Collaborative International Dictionary of English

  • sequent — index consecutive, corollary, derivative, future, outcome, proximate, subsequent, successive Burton s Legal …   Law dictionary

  • sequent — [sē′kwənt] adj. [L sequens, prp. of sequi, to follow < IE base * sekw , to follow > OE secg, warrior] 1. following in time or order; subsequent 2. following as a result or effect; consequent n. something that follows, esp. as a result;… …   English World dictionary

  • sequent — adjective Etymology: Latin sequent , sequens, present participle Date: 1601 1. consecutive, succeeding 2. consequent, resultant …   New Collegiate Dictionary

  • sequent — sequently, adv. /see kweuhnt/, adj. 1. following; successive. 2. following logically or naturally; consequent. 3. characterized by continuous succession; consecutive. n. 4. something that follows in order or as a result. [1550 60; < L sequent (s …   Universalium

  • sequent — 1. adjective /ˈsiːkwənt/ a) The follows on as a result, conclusion etc.; consequent , , . Maisie found herself clutched to her mothers breast and passionately sobbed and shrieked over, made the subject of a demonstration evidently sequent to some …   Wiktionary

  • sequent — se•quent [[t]ˈsi kwənt[/t]] adj. 1) following; successive 2) characterized by continuous succession; consecutive • Etymology: 1550–60; < L sequent , s. of sequēns, prp. of sequī to follow; see ent …   From formal English to slang

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”