View source for Sequent calculus

One of the formulations of the [[Predicate calculus|predicate calculus]]. Due to the convenient representation of derivations, the sequent calculus has wide applications in [[Proof theory|proof theory]], in the foundations of mathematics and in the automatic search for a deduction. The sequent calculus was introduced by G. Gentzen in 1934 (see [[#References|[1]]]). One version of the classical calculus of predicates in the form of the sequent calculus is presented below.

A collection of formulas is a finite set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s0845801.png" /> of formulas of a certain logico-mathematical language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s0845802.png" />, where in this set, repetitions of formulas are permitted. The order of the formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s0845803.png" /> is inessential, but for each formula, the number of copies of it that are in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s0845804.png" /> is given. The collection of formulas can be empty. The set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s0845805.png" /> is obtained from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s0845806.png" /> by adjoining a copy of the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s0845807.png" />. For two collections of formulas <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s0845808.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s0845809.png" />, a figure of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458010.png" /> is called a sequent; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458011.png" /> is called the antecedent and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458012.png" /> the successor of the sequent.

The axioms of the sequent calculus have the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458013.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458014.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458015.png" /> are arbitrary collections of formulas and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458016.png" /> is an arbitrary atomic (elementary) formula. The derivation rules of the calculus have a very symmetrical structure; logical connectives are introduced into the sequent calculus by the following schemata:

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458017.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458018.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458019.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458020.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458021.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458022.png" /></td> </tr></table>

In the rules <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458023.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458024.png" /> it is assumed that the variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458025.png" /> is not free in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458026.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458027.png" />, and that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458028.png" /> is not free in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458029.png" />.

The sequent calculus is equivalent to the usual form of predicate calculus, in the sense that a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458030.png" /> is deducible in the predicate calculus if and only if the sequent <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458031.png" /> is deducible in the sequent calculus. The fundamental theorem of Gentzen (or the normalization theorem) is essential for the proof of this assertion; this theorem can be stated as follows: If the sequents <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458032.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458033.png" /> are deducible in the sequent calculus, then so is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458034.png" />. The derivation rule

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458035.png" /></td> </tr></table>

is called the cut rule, and the normalization theorem asserts that the cut rule is admissible in the sequent calculus, or that the addition of the cut rule does not change the collection of deducible sequents. In view of this, Gentzen's theorem is also called the cut-elimination theorem.

The symmetric structure of the sequent calculus greatly facilitates the study of its properties. Therefore, an important place in proof theory is occupied by the search for sequent variants of applied calculi: arithmetic, analysis, type theory, and also the proof for such calculi of the cut-elimination theorem in one form or another (see [[#References|[2]]], [[#References|[3]]]). Sequent variants can also be found for many calculi based on non-classical logics: intuitionistic, modal, relevance logics, and others (see [[#References|[3]]], [[#References|[4]]]).

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  G. Gentzen,   "Untersuchungen über das logische Schliessen"  ''Math. Z.'' , '''39'''  (1935)  pp. 176–210; 405–431  ((English translation: The collected papers of Gerhard Gentzen, North-Holland, 1969; edited by M.E. Szabo))</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  G. Takeuti,   "Proof theory" , North-Holland  (1975)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  A.G. Dragalin,   "Mathematical intuitionism. Introduction to proof theory" , Amer. Math. Soc.  (1988)  (Translated from Russian)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  R. Feys,   "Modal logics" , Gauthier-Villars  (1965)</TD></TR></table>



====Comments====
Intuitively, the sequent <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458036.png" /> expresses that if all the formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458037.png" /> hold, then at least one of those in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084580/s08458038.png" /> must also hold.

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  M.E. Szabo,   "Algebra of proofs" , North-Holland  (1978)</TD></TR></table>