Sequents, Calculus of

(or sequential calculus, calculus of methods of inference), a modification of the concept of a logical calculus. In the calculus of sequents, the basic objects that are dealt with are not formulas but sequents—that is, expressions of the form A₁,…, A_l → B₁,…, B_m, where → is analogous to the deducibility symbol and A_l…, A_l and B_l, …, B_m are arbitrary formulas. The formulas A₁ …, A_l constitute the antecedent of the sequent, and the formulas B₁, …, B_m make up its succedent.

When l, m ≥ 1, the sequent A_l …, A_l → B_l, … B_m is interpreted as the formula

A_l& … &A_l⊃ B_lV … VB_m

where & is the symbol of conjunction, ⊃ of implication, and v of disjunction (seeLOGICAL OPERATIONS). In addition, a sequent with an empty antecedent is interpreted as a truth, a sequent with an empty succedent is interpreted as a falsehood, and, consequently, the sequent →, consisting of just the arrow, is interpreted as a contradiction. All sequents of the form C → C, and only such sequents, are axioms, or initial sequents, in the calculus of sequents.

The rules of inference are divided into structural and logical rules. The former codify permissible changes in the arrangement of the formulas of the antecedent and succedent, and the latter codify the introduction of various logical symbols into the sequents. The structural rules are as follows: refinement, which is the addition of an arbitrary formula to an antecedent or succedent; contraction, which is the deletion of repeating formulas; the transposition of arbitrary formulas in the antecedent or succedent; and the cut rule, that is,

Here, the Latin letters denote arbitrary formulas, and the Greek letters denote rows of formulas, which are divided by the commas; the premises of the rule are written above the line, and the conclusion below it. The logical rules of inference have the following form for the sequential classical propositional calculus:

If both the structural and logical rules of inference are restricted by the condition that the succedent of each sequent must contain no more than one formula, then we obtain the sequential intuitionistic propositional calculus. This condition is sufficient for the nondeducibility of the law of the excluded middle and of the law of the removal of a double negation in the calculus of sequents. The sequential predicate calculus is obtained by appending to the preceding rules two more pairs of rules for the introduction of the universal and existential quantifiers.

The fundamental result of the German mathematician G. Gentzen consists in the establishment of the possibility of reducing every derivation in the calculus of sequents to a normal form that does not contain applications of the cut rule and that thus in a sense represents a direct derivation. This result has numerous applications. Particularly important are the proofs of the consistency of arithmetic formal systems. These proofs make use of mathematical apparatus that goes beyond the framework of Hilbert’s finitism (seeAXIOMATIC METHOD and METAMATHEMATICS) and thus in a sense bypass the difficulties resulting from K. Gödel’s theorem of the incompleteness of formal arithmetic. Gentzen’s fundamental theorem underlies most algorithms of deducibility for logical and logico-mathematical calculi. This fact accounts for the exceptional importance of the calculus of sequents for the intensively developing research in the field of computerized theorem proving; such research is an important example of the modeling of human mental activity.