Sequent calculus

One of the formulations of the predicate calculus. Due to the convenient representation of derivations, the sequent calculus has wide applications in 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 [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 of formulas of a certain logico-mathematical language , where in this set, repetitions of formulas are permitted. The order of the formulas in is inessential, but for each formula, the number of copies of it that are in is given. The collection of formulas can be empty. The set is obtained from by adjoining a copy of the formula . For two collections of formulas and , a figure of the form is called a sequent; is called the antecedent and the successor of the sequent.

The axioms of the sequent calculus have the form , where and are arbitrary collections of formulas and 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:

In the rules and it is assumed that the variable is not free in or , and that is not free in .

The sequent calculus is equivalent to the usual form of predicate calculus, in the sense that a formula is deducible in the predicate calculus if and only if the sequent 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 and are deducible in the sequent calculus, then so is . The derivation rule

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 [2], [3]). Sequent variants can also be found for many calculi based on non-classical logics: intuitionistic, modal, relevance logics, and others (see [3], [4]).

References

[1]	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))
[2]	G. Takeuti, "Proof theory" , North-Holland (1975)
[3]	A.G. Dragalin, "Mathematical intuitionism. Introduction to proof theory" , Amer. Math. Soc. (1988) (Translated from Russian)
[4]	R. Feys, "Modal logics" , Gauthier-Villars (1965)

Comments

Intuitively, the sequent expresses that if all the formulas in hold, then at least one of those in must also hold.

References

[a1]	M.E. Szabo, "Algebra of proofs" , North-Holland (1978)