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 $\mathrm{\Gamma }$ of formulas of a certain logico-mathematical language $\mathrm{\Omega }$, where in this set, repetitions of formulas are permitted. The order of the formulas in $\mathrm{\Gamma }$ is inessential, but for each formula, the number of copies of it that are in $\mathrm{\Gamma }$ is given. The collection of formulas can be empty. The set $\varphi \mathrm{\Gamma }$ is obtained from $\mathrm{\Gamma }$ by adjoining a copy of the formula $\varphi$. For two collections of formulas $\mathrm{\Gamma }$ and $\mathrm{\Delta }$, a figure of the form $\mathrm{\Gamma }\to \mathrm{\Delta }$ is called a sequent; $\mathrm{\Gamma }$ is called the antecedent and $\mathrm{\Delta }$ the successor of the sequent.

The axioms of the sequent calculus have the form $\varphi \mathrm{\Gamma }\to \mathrm{\Delta }\varphi$, where $\mathrm{\Gamma }$ and $\mathrm{\Delta }$ are arbitrary collections of formulas and $\varphi$ 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:

$$(\wedge \to )\frac{\varphi \psi \mathrm{\Gamma }\to \mathrm{\Delta }}{(\varphi \wedge \psi )\mathrm{\Gamma }\to \mathrm{\Delta }};(\to \wedge )\frac{\mathrm{\Gamma }\to \mathrm{\Delta }\varphi ;\mathrm{\Gamma }\to \mathrm{\Delta }\psi }{\mathrm{\Gamma }\to \mathrm{\Delta }(\varphi \wedge \psi )};$$

$$(\vee \to )\frac{\varphi \mathrm{\Gamma }\to \mathrm{\Delta };\psi \mathrm{\Gamma }\to \mathrm{\Delta }}{(\varphi \vee \psi )\mathrm{\Gamma }\to \mathrm{\Delta }};(\to \vee )\frac{\mathrm{\Gamma }\to \mathrm{\Delta }\varphi \psi }{\mathrm{\Gamma }\to \mathrm{\Delta }(\varphi \vee \psi )};$$

$$(\supseteq \to )\frac{\mathrm{\Gamma }\to \mathrm{\Delta }\varphi ;\psi \mathrm{\Gamma }\to \mathrm{\Delta }}{(\varphi \supseteq \psi )\mathrm{\Gamma }\to \mathrm{\Delta }};(\to \supseteq )\frac{\varphi \mathrm{\Gamma }\to \mathrm{\Delta }\psi }{\mathrm{\Gamma }\to \mathrm{\Delta }(\varphi \supseteq \psi )};$$

$$(\mathrm{\neg }\to )\frac{\mathrm{\Gamma }\to \mathrm{\Delta }\varphi }{\mathrm{\neg }\varphi \mathrm{\Gamma }\to \mathrm{\Delta }};(\to \mathrm{\neg })\frac{\varphi \mathrm{\Gamma }\to \mathrm{\Delta }}{\mathrm{\Gamma }\to \mathrm{\Delta }\mathrm{\neg }\varphi };$$

$$(\mathrm{\forall }\to )\frac{\mathrm{\forall }x\varphi \varphi (x\mid t)\mathrm{\Gamma }\to \mathrm{\Delta }}{\mathrm{\forall }x\varphi \mathrm{\Gamma }\to \mathrm{\Delta }};(\to \mathrm{\forall })\frac{\mathrm{\Gamma }\to \mathrm{\Delta }\varphi }{\mathrm{\Gamma }\to \mathrm{\Delta }\mathrm{\forall }x\varphi (y\mid x)};$$

$$(\mathrm{\exists }\to )\frac{\varphi \mathrm{\Gamma }\to \mathrm{\Delta }}{\mathrm{\exists }x\varphi (y\mid x)\mathrm{\Gamma }\to \mathrm{\Delta }};(\to \mathrm{\exists })\frac{\mathrm{\Gamma }\to \mathrm{\Delta }\varphi (x\mid t)\mathrm{\exists }x\varphi }{\mathrm{\Gamma }\to \mathrm{\Delta }\mathrm{\exists }x\varphi }.$$

In the rules $(\to \mathrm{\forall })$ and $(\mathrm{\exists }\to )$ it is assumed that the variable $y$ is not free in $\mathrm{\Gamma }$ or $\mathrm{\Delta }$, and that $x$ is not free in $\varphi$.

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

$$\frac{\mathrm{\Gamma }\to \mathrm{\Delta }\varphi ;\varphi \mathrm{\Gamma }\to \mathrm{\Delta }}{\mathrm{\Gamma }\to \mathrm{\Delta }}$$

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[edit]

Comments[edit]

Intuitively, the sequent $\mathrm{\Gamma }\to \mathrm{\Delta }$ expresses that if all the formulas in $\mathrm{\Gamma }$ hold, then at least one of those in $\mathrm{\Delta }$ must also hold.

References[edit]