View source for Sequent

{{Short description|Logical proof involving antecedents and consequents}}
{{other uses}}
In [[mathematical logic]], a '''sequent''' is a very general kind of conditional assertion.

: <math>A_1,\,\dots,A_m \,\vdash\, B_1,\,\dots,B_n.</math>

A sequent may have any number ''m'' of condition [[Well-formed formula|formulas]] ''A<sub>i</sub>'' (called "[[Antecedent (logic)|antecedents]]") and any number ''n'' of asserted formulas ''B<sub>j</sub>'' (called "succedents" or "[[consequent]]s"). A sequent is understood to mean that if all of the antecedent conditions are true, then at least one of the consequent formulas is true. This style of conditional assertion is almost always associated with the conceptual framework of [[sequent calculus]].

== Introduction ==

=== The form and semantics of sequents ===

Sequents are best understood in the context of the following three kinds of [[Judgment (mathematical logic)|logical judgments]]:
<ol>
<li>'''Unconditional assertion'''. No antecedent formulas.
* Example:  ⊢ ''B''
* Meaning: ''B'' is true.
<li>'''Conditional assertion'''. Any number of antecedent formulas.
<ol type="a">
<li>'''Simple conditional assertion'''. Single consequent formula.
* Example: ''A<sub>1</sub>'', ''A<sub>2</sub>'', ''A<sub>3</sub>'' ⊢ ''B''
* Meaning: IF ''A<sub>1</sub>'' AND ''A<sub>2</sub>'' AND ''A<sub>3</sub>'' are true, THEN ''B'' is true.
<li>'''Sequent'''. Any number of consequent formulas. 
* Example: ''A<sub>1</sub>'', ''A<sub>2</sub>'', ''A<sub>3</sub>'' ⊢ ''B<sub>1</sub>'', ''B<sub>2</sub>'', ''B<sub>3</sub>'', ''B<sub>4</sub>''
* Meaning: IF ''A<sub>1</sub>'' AND ''A<sub>2</sub>'' AND ''A<sub>3</sub>''  are true, THEN ''B<sub>1</sub>'' OR ''B<sub>2</sub>'' OR ''B<sub>3</sub>'' OR ''B<sub>4</sub>'' is true.
</ol>
</ol>
Thus sequents are a generalization of simple conditional assertions, which are a generalization of unconditional assertions.

The word "OR" here is the [[logical disjunction|inclusive OR]].<ref>The disjunctive semantics for the right side of a sequent is stated and explained by {{harvnb|Curry|1977|pp=189–190}}, {{harvnb|Kleene|2002|pp=290, 297}}, {{harvnb|Kleene|2009|p=441}}, {{harvnb|Hilbert|Bernays|1970|p=385}}, {{harvnb|Smullyan|1995|pp=104–105}}, {{harvnb|Takeuti|2013|p=9}}, and {{harvnb|Gentzen|1934|p=180}}.</ref> The motivation for disjunctive semantics on the right side of a sequent comes from three main benefits.
# The symmetry of the classical [[rule of inference|inference rules]] for sequents with such semantics.
# The ease and simplicity of converting such classical rules to intuitionistic rules.
# The ability to prove completeness for predicate calculus when it is expressed in this way.
All three of these benefits were identified in the founding paper by {{harvtxt|Gentzen|1934|p=194}}.

Not all authors have adhered to Gentzen's original meaning for the word "sequent". For example, {{harvtxt|Lemmon|1965}} used the word "sequent" strictly for simple conditional assertions with one and only one consequent formula.<ref name=Lemmon1965p12>{{harvnb|Lemmon|1965|p=12}}, wrote: "Thus a sequent is an argument-frame containing a set of assumptions and a conclusion which is claimed to follow from them. [...] The propositions to the left of '⊢' become assumptions of the argument, and the proposition to the right becomes a conclusion validly drawn from those assumptions."</ref> The same single-consequent definition for a sequent is given by {{harvnb|Huth|Ryan|2004|p=5}}.

=== Syntax details ===
In a general sequent of the form
:<math>\Gamma\vdash\Sigma</math>
both Γ and Σ are [[sequence]]s of logical formulas, not [[set (mathematics)|sets]]. Therefore both the number and order of occurrences of formulas are significant. In particular, the same formula may appear twice in the same sequence. The full set of [[Sequent calculus#Inference rules|sequent calculus inference rules]] contains rules to swap adjacent formulas on the left and on the right of the assertion symbol (and thereby arbitrarily [[Permutation|permute]] the left and right sequences), and also to insert arbitrary formulas and remove duplicate copies within the left and  the right sequences. (However, {{harvtxt|Smullyan|1995|pp=107–108}}, uses ''sets'' of formulas in sequents instead of sequences of formulas. Consequently the three pairs of ''structural rules'' called "thinning", "contraction" and "interchange" are not required.)

The symbol ' <math>\vdash</math> ' is often referred to as the "[[Turnstile (symbol)|turnstile]]", "right tack", "tee", "assertion sign" or "assertion symbol". It is often read, suggestively, as "yields", "proves" or "entails".

=== Properties ===

==== Effects of inserting and removing propositions ====
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. This is one of the symmetry advantages which follows from the use of disjunctive semantics on the right hand side of the assertion symbol, whereas conjunctive semantics is adhered to on the left hand side.

==== Consequences of empty lists of formulas ====
In the extreme case where the list of ''antecedent'' formulas of a sequent is empty, the consequent is unconditional. This differs from the simple unconditional assertion because the number of consequents is arbitrary, not necessarily a single consequent. Thus for example, ' ⊢ ''B<sub>1</sub>'', ''B<sub>2</sub>'' ' means that either ''B<sub>1</sub>'', or  ''B<sub>2</sub>'', or both must be true. An empty antecedent formula list is equivalent to the "always true" proposition, called the "[[Tautology (logic)|verum]]", denoted "⊤". (See [[Tee (symbol)]].)

In the extreme case where the list of ''consequent'' formulas of a sequent is empty, the rule is still that at least one term on the right  be true, which is clearly [[Contradiction|impossible]]. This is signified by the 'always false' proposition, called the "[[False (logic)|falsum]]", denoted "⊥". Since the consequence is false, at least one of the antecedents must be false. Thus for example, ' ''A<sub>1</sub>'', ''A<sub>2</sub>'' ⊢ ' means that at least one of the antecedents ''A<sub>1</sub>'' and ''A<sub>2</sub>'' must be false.

One sees here again a symmetry because of the disjunctive semantics on the right hand side. If the left side is empty, then one or more right-side propositions must be true. If the right side is empty, then one or more of the left-side propositions must be false.

The doubly extreme case ' ⊢ ', where both the antecedent and consequent lists of formulas are empty is "[[Interpretation (logic)#Non-empty domain requirement|not satisfiable]]".<ref>{{harvnb|Smullyan|1995|p=105}}.</ref> In this case, the meaning of the sequent is effectively ' ⊤ ⊢ ⊥  '. This is equivalent to the sequent ' ⊢ ⊥ ', which clearly cannot be valid.

=== Examples ===
A sequent of the form ' ⊢ α, β ', for logical formulas α and β, means that either α is true or β is true (or both). But it does not mean that either α is a tautology or β is a tautology. To clarify this, consider the example ' ⊢ B ∨ A, C ∨ ¬A '. This is a valid sequent because either B ∨ A is true or C ∨ ¬A is true. But neither of these expressions is a tautology in isolation. It is the ''disjunction'' of these two expressions which is a tautology.

Similarly, a sequent of the form ' α, β ⊢ ', for logical formulas α and β, means that either α is false or β is false. But it does not mean that either α is a contradiction or β is a contradiction. To clarify this, consider the example ' B ∧ A, C ∧ ¬A ⊢ '. This is a valid sequent because either B ∧ A is false or C ∧ ¬A is false. But neither of these expressions is a contradiction in isolation. It is the ''conjunction'' of these two expressions which is a contradiction.

=== 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 [[Coplanarity|line]]. This rule indicates that if everything above the line is true, so is everything under the line.

A typical rule is:

:<math> \frac{\Gamma,\alpha\vdash\Sigma\qquad \Gamma\vdash\alpha}{\Gamma\vdash\Sigma}</math>

This indicates that if we can deduce that <math>\Gamma,\alpha</math> yields <math>\Sigma</math>, and that <math>\Gamma</math> yields <math>\alpha</math>, then we can also deduce that <math>\Gamma</math> yields  <math>\Sigma</math>. (See also the full set of [[sequent calculus#Inference rules|sequent calculus inference rules]].)

== Interpretation ==

=== History of the meaning of sequent assertions ===
The assertion symbol in sequents originally meant exactly the same as the implication operator. But over time, its meaning has changed to signify provability within a theory rather than semantic truth in all models.

In 1934, Gentzen did not define the assertion symbol ' ⊢ ' in a sequent to signify provability. He defined it to mean exactly the same as the implication operator ' ⇒ '. Using ' → ' instead of ' ⊢ ' and ' ⊃ ' instead of ' ⇒ ', he wrote: "The sequent A<sub>1</sub>, ..., A<sub>μ</sub> → B<sub>1</sub>, ..., B<sub>ν</sub> signifies, as regards content, exactly the same as the formula (A<sub>1</sub> &amp; ... &amp; A<sub>μ</sub>) ⊃ (B<sub>1</sub> ∨ ... ∨ B<sub>ν</sub>)".<ref>{{harvnb|Gentzen|1934|p=180}}.
: 2.4. Die Sequenz A<sub>1</sub>, ..., A<sub>μ</sub> → B<sub>1</sub>, ..., B<sub>ν</sub> bedeutet inhaltlich genau dasselbe wie die Formel
::: (A<sub>1</sub> &amp; ... &amp; A<sub>μ</sub>) ⊃ (B<sub>1</sub> ∨ ... ∨ B<sub>ν</sub>).</ref> (Gentzen employed the right-arrow symbol between the antecedents and consequents of sequents. He employed the symbol ' ⊃ ' for the logical implication operator.)

In 1939, [[David Hilbert|Hilbert]] and [[Paul Bernays|Bernays]] stated likewise that a sequent has the same meaning as the corresponding implication formula.<ref>{{harvnb|Hilbert|Bernays|1970|p=385}}.
: Für die inhaltliche Deutung ist eine Sequenz
::: A<sub>1</sub>, ..., A<sub>r</sub> → B<sub>1</sub>, ..., B<sub>s</sub>,
: worin die Anzahlen r und s von 0 verschieden sind, gleichbedeutend mit der Implikation
::: (A<sub>1</sub> &amp; ... &amp; A<sub>r</sub>) → (B<sub>1</sub> ∨ ... ∨ B<sub>s</sub>)
</ref>

In 1944, [[Alonzo Church]] emphasized that Gentzen's sequent assertions did not signify provability.

: "Employment of the deduction theorem as primitive or derived rule must not, however, be confused with the use of ''Sequenzen'' by Gentzen. For Gentzen's arrow, →, is not comparable to our syntactical notation, ⊢, but belongs to his object language (as is clear from the fact that expressions containing it appear as premisses and conclusions in applications of his rules of inference)."<ref>{{harvnb|Church|1996|p=165}}.</ref>

Numerous publications after this time have stated that the assertion symbol in sequents does signify provability within the theory where the sequents are formulated. [[Haskell Curry|Curry]] in 1963,<ref>{{harvnb|Curry|1977|p=184}}</ref> [[John Lemmon|Lemmon]] in 1965,<ref name=Lemmon1965p12 /> and Huth and Ryan in 2004<ref>{{harvtxt|Huth|Ryan|2004|p=5}}</ref> all state that the sequent assertion symbol signifies provability. However, {{harvtxt|Ben-Ari|2012|p=69}} states that the assertion symbol in Gentzen-system sequents, which he denotes as ' ⇒ ', is part of the object language, not the metalanguage.<ref>{{harvnb|Ben-Ari|2012|p=69}}, defines sequents to have the form ''U'' ⇒ ''V'' for (possibly non-empty) sets of formulas ''U'' and ''V''. Then he writes:
: "Intuitively, a sequent represents 'provable from' in the sense that the formulas in ''U'' are assumptions for the set of formulas ''V'' that are to be proved. The symbol ⇒ is similar to the symbol ⊢ in Hilbert systems, except that ⇒ is part of the object language of the deductive system being formalized, while ⊢ is a metalanguage notation used to reason about deductive systems."</ref>

According to [[Dag Prawitz|Prawitz]] (1965): "The calculi of sequents can be understood as meta-calculi for the deducibility relation in the corresponding systems of natural deduction."<ref>{{harvnb|Prawitz|2006|p=90}}.</ref> And furthermore: "A proof in a calculus of sequents can be looked upon as an instruction on how to construct a corresponding natural deduction."<ref>See {{harvnb|Prawitz|2006|p=91}}, for this and further details of interpretation.</ref> In other words, the assertion symbol is part of the object language for the sequent calculus, which is a kind of meta-calculus, but simultaneously signifies deducibility in an underlying natural deduction system.

=== Intuitive meaning ===
{{Refimprove section|date=June 2014|talk=Assertion symbols in sequents do not signify provability.}}
A sequent is a [[Formalism (mathematics)|formalized]] statement of [[Proof theory|provability]] that is frequently used when specifying [[proof calculus|calculi]] for [[deductive reasoning|deduction]]. In the sequent calculus, the name ''sequent'' is used for the construct, which can be regarded as a specific kind of [[Judgment (mathematical logic)|judgment]], characteristic to this deduction system.

The intuitive meaning of the sequent <math>\Gamma\vdash\Sigma</math> is that under the assumption of Γ the conclusion of Σ is provable. Classically, the formulae on the left of the turnstile can be interpreted [[logical conjunction|conjunctively]] while the formulae on the right can be considered as a [[logical disjunction|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. <math>\Gamma\vdash</math> means that Γ proves falsity and is thus inconsistent. On the other hand an empty antecedent is assumed to be true, i.e., <math>\vdash\Sigma</math> 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]].

Of course, other intuitive explanations are possible, which are classically equivalent.  For example, <math>\Gamma\vdash\Sigma</math> can be read as asserting that it cannot be the case that every formula in Γ is true and every formula in Σ is false (this is related to the double-negation interpretations of classical [[intuitionistic logic]], such as [[Glivenko's translation|Glivenko's theorem]]).

In any case, these intuitive readings are only pedagogical. Since formal proofs in proof theory are purely [[syntax|syntactic]], the [[semantics|meaning]] of (the derivation of) a sequent is only given by the properties of the calculus that provides the actual [[rule of inference|rules of inference]].

Barring any contradictions in the technically precise definition above we can describe sequents in their introductory logical form. <math>\Gamma</math> represents a set of assumptions that we begin our logical process with, for example "Socrates is a man" and "All men are mortal". The <math>\Sigma</math> 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 <math>\Sigma</math> side of the ''turnstile''. In this sense, <math>\vdash</math> means the process of reasoning, or "therefore" in English.

== Variations ==
{{Refimprove section|date=June 2014}}
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 (although multi-succedent calculi for intuitionistic logic are also possible). More precisely, the restriction of the general sequent calculus to single-succedent-formula sequents, ''with the same inference rules'' as for general sequents, constitutes an intuitionistic sequent calculus. (This restricted sequent calculus is denoted LJ.)

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 [[multiset]]s or [[Set (mathematics)|sets]] instead of sequences. Thus one disregards the order or even the numbers 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 do not depend on these data. In [[substructural logic]], however, this may become quite important.

[[Natural deduction]] systems use single-consequence conditional assertions, but they typically do not use the same sets of inference rules as Gentzen introduced in 1934. In particular, [[System L|tabular natural deduction]] systems, which are very convenient for practical theorem-proving in propositional calculus and predicate calculus, were applied by {{harvtxt|Suppes|1999}} and {{harvtxt|Lemmon|1965}} for teaching introductory logic in textbooks.

== Etymology ==
Historically, sequents have been introduced by [[Gerhard Gentzen]] in order to specify his famous [[sequent calculus]].<ref>{{harvnb|Gentzen|1934}}, {{harvnb|Gentzen|1935}}.</ref> 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.

Kleene<ref>{{harvnb|Kleene|2002|p=441}}</ref> makes the following comment on the translation into English: "Gentzen says 'Sequenz', which we translate as 'sequent', because we have already used 'sequence' for any succession of objects, where the German is 'Folge'."

== See also ==
*[[Gerhard Gentzen]]
*[[Intuitionistic logic]] 
*[[Natural deduction]]
*[[Sequent calculus]]

==Notes==
{{Reflist}}

==References==
* {{cite book|last1=Ben-Ari|first1=Mordechai|author1-link=Mordechai Ben-Ari|title=Mathematical logic for computer science|publisher=Springer|location=London|year=2012|orig-year=1993|isbn=978-1-4471-4128-0}}
* {{cite book|last1=Church|first1=Alonzo|author1-link=Alonzo Church|title=Introduction to mathematical logic|publisher=Princeton University Press|location=Princeton, New Jersey|orig-year=1944|year=1996|isbn=978-0-691-02906-1}}
* {{cite book|last1=Curry|first1=Haskell Brooks|author1-link=Haskell Curry|title=Foundations of mathematical logic|orig-year=1963|year=1977|publisher=Dover Publications Inc.|location=New York|isbn=978-0-486-63462-3}}
* {{Cite journal|last1=Gentzen|first1=Gerhard|author1-link=Gerhard Gentzen|title=Untersuchungen über das logische Schließen. I|journal=Mathematische Zeitschrift|volume=39|year=1934|issue=2|pages=176–210|doi=10.1007/bf01201353|s2cid=121546341 |url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375508}}
* {{Cite journal|last1=Gentzen|first1=Gerhard|author1-link=Gerhard Gentzen|title=Untersuchungen über das logische Schließen. II|journal=Mathematische Zeitschrift|volume=39|year=1935|issue=3|pages=405–431|doi=10.1007/bf01201363|s2cid=186239837 |url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375605}}
* {{cite book|last1=Hilbert|first1=David| author1-link=David Hilbert | last2=Bernays | first2=Paul |author2-link=Paul Bernays|title=Grundlagen der Mathematik II|orig-year=1939|year=1970|publisher=Springer-Verlag|location=Berlin, New York|isbn=978-3-642-86897-9|edition=Second}}
* {{cite book|last1=Huth|first1=Michael|last2=Ryan|first2=Mark|title=Logic in Computer Science| year=2004|publisher=Cambridge University Press|location=Cambridge, United Kingdom|edition=Second|isbn=978-0-521-54310-1}}
* {{cite book|last1=Kleene|first1=Stephen Cole|author1-link=Stephen Cole Kleene|title=Introduction to metamathematics|orig-year=1952|year=2009|publisher=Ishi Press International|isbn=978-0-923891-57-2}}
* {{cite book|last1=Kleene|first1=Stephen Cole|author1-link=Stephen Cole Kleene|title=Mathematical logic|orig-year=1967|year=2002|publisher=Dover Publications|location=Mineola, New York|isbn=978-0-486-42533-7}}
* {{cite book|last1=Lemmon|first1=Edward John|author1-link=John Lemmon|title=Beginning logic|year=1965|publisher=Thomas Nelson|isbn=0-17-712040-1}}
* {{Prawitz Natural Deduction|2006}} {{sfn whitelist|CITEREFPrawitz2006}}
* {{cite book|last1=Smullyan|first1=Raymond Merrill|author1-link=Raymond Smullyan|year=1995|orig-year=1968|title=First-order logic|publisher=Dover Publications|location=New York|isbn=978-0-486-68370-6}}
* {{cite book|last1=Suppes|first1=Patrick Colonel|author1-link=Patrick Suppes|year=1999|orig-year=1957|title=Introduction to logic|publisher=Dover Publications|location=Mineola, New York|isbn=978-0-486-40687-9}}
* {{cite book|last1=Takeuti|first1=Gaisi|author1-link=Gaisi Takeuti|title=Proof theory|edition=Second|publisher=Dover Publications|location=Mineola, New York|year=2013|orig-year=1975|isbn=978-0-486-49073-1}}

==External links==
* {{springer|title=Sequent (in logic)|id=p/s084590}}

[[Category:Proof theory]]
[[Category:Logical expressions]]