Sequent Calculus

A sequent is an expression , where  and  are (possibly empty) sequences of formulas. Here,  is called the antecedent and  is called the consequent. The informal understanding of sequents is that the sequent  corresponds to . The initial sequent of all derivations is

(1)

The rules of inference for sequent calculus are divided in two categories: structural and logical. There are at least two logical rules for every propositional connective and every quantifier; one of them applies to the antecedent, whereas the other applies to the consequent. The structural rules are thinning,

(2)

contraction,

(3)

exchange,

(4)

and cut,

(5)

The logical rules are given by conjunction,

(6)

disjunction,

(7)

negation,

(8)

implication,

(9)

universal quantifier,

(10)

and existential quantifier

(11)

Here, the variable  is free in  and  is obtained from  by replacing all free occurrences of  by . The variable  occurring in the -succedent rule and the -antecedent rule is called the eigenvariable. It may not occur in the lower sequents of the respective rules.

Sequent calculus specifies classical first-order logic, and the same framework can also be used to specify intuitionistic logic. In order to limit derivations to intuitionistic ones, the additional constraint that every succedent may have not more one formula is added. The classical (multi-succedent) variant due to Gentzen is called LK, and the intuitionistic (single-succedent) variant is called LJ. LK can alternatively be defined as single-succedent calculus augmented with the law of excluded middle as yet another basic sequent. Proof theories based on sequent rules of inference are also called Gentzen-type. Many other logic formulations based on sequents have been introduced subsequently.

A sample derivation is provided by double negation, which is valid in the classical variant of the sequent calculus but not in the intuitionistic one.

A second derivation (which is a valid intuitionistic derivation) is shown above.

Sequent calculus is a very useful tool for proof theory, primarily because of the admissibility of the cut rule, which can be eliminated from derivations without affecting the set of derivable formulas.

REFERENCES

Gentzen, G. The Collected Papers of Gerhard Gentzen (Ed. M. E. Szabo). Amsterdam, Netherlands: North-Holland, 1969.

Kleene, S. C. Introduction to Metamathematics. Princeton, NJ: Van Nostrand, 1964.