Lecture
A sequention (Eng. sequention) is an ordered binary sequence in asynchronous sequential logic.
A sequent (proof theory) (Eng. sequent, Ger. sequenz) is a formula of a Gentzen-style calculus in proof theory.
A sequent is an expression of the form 
, where 
and 
are finite (possibly empty) sequences of logical formulas called cedents: is the antecedent, and is the succedent (sometimes the consequent). The intuitive meaning assigned to the sequent 
is: if the conjunction of the antecedent formulas 
holds, then the disjunction of the succedent formulas 
holds (is derivable). Sometimes, instead of the arrow, the sequent notation uses the derivability sign (
) or the implication sign (
).
If the antecedent is empty (
), then the disjunction of the succedent formulas is assumed to hold; an empty succedent (
) is interpreted as the conjunction of the antecedent formulas being contradictory. An empty sequent 
means that the system under consideration contains a contradiction. The order of the formulas in the cedents is not significant, but the number of occurrences of a formula instance in a cedent does matter. Writing a cedent as 
or 
, where is a sequence of formulas and 
is a formula, denotes adding the formula to the cedent (possibly as a further occurrence).
Axioms are the initial sequents accepted without proof; in the sequent-calculus approach the number of axioms is minimized, so that in the Gentzen systems 
and 
only a single axiom scheme is given, 
. Inference rules in sequent form are written as the following expressions:
and 
,
they are interpreted as an assertion about the derivability, from the upper sequent 
(upper sequents and 
), of the lower sequent 
. A proof in sequent calculi (as in natural-deduction systems) is written in tree form from top to bottom, for example:
,
where each horizontal line denotes an immediate inference — a transition from the upper sequents to the lower one according to one of the inference rules adopted in the given system. Thus, the existence of a derivation tree that starts from axioms (initial sequents) and leads to the sequent 
means that it is derivable in the given logical system: 
.
Sequent calculus is a variant of logical calculi that, to prove statements, uses not arbitrary chains of tautologies but sequences of conditional judgments — sequents[⇨]. The best-known sequent calculi — 
[⇨] and 
[⇨] for classical and intuitionistic predicate calculus, respectively — were constructed by Gentzen in 1934; sequent-style variants were later formulated for a broad class of applied calculi (arithmetic, analysis), type theories, and non-classical logics.
In the sequent-calculus approach, instead of broad sets of axioms, elaborate systems of inference rules are used, and the proof is carried out in the form of a derivation tree; on this basis (together with natural-deduction systems) sequent calculi belong to the Gentzen type, as opposed to axiomatic Hilbert-style calculi[en], in which, given an elaborate set of axioms, the number of inference rules is reduced to a minimum.
The main property of the sequent form is its symmetric structure[⇨], which makes it convenient to prove cut elimination, and, as a consequence, sequent calculi are the primary systems studied in proof theory.
The concept of the sequent, for systematic use in proofs in the form of a derivation tree, was introduced in 1929 by the German physicist and logician Paul Hertz (1881—1940) , though no complete calculus for any particular logical theory was built in his work . In a 1932 paper, Gentzen attempted to develop Hertz's approach , but in 1934 he abandoned Hertz's groundwork: he introduced the natural-deduction systems 
and 
for classical and intuitionistic predicate calculus respectively, which use ordinary tautologies and derivation trees, and, as their structural development, the sequent systems and . For and Gentzen proved cut elimination, which gave a significant methodological boost to the proof theory outlined by Hilbert: in the same paper Gentzen was the first to prove the completeness of intuitionistic predicate calculus, and in 1936 he proved the consistency of Peano arithmetic for the integers, extending it by means of the sequent variant with transfinite induction up to the ordinal 
. This last result also carried special ideological significance in light of the pessimism of the early 1930s stemming from Gödel's incompleteness theorem, according to which the consistency of arithmetic cannot be established by arithmetic's own means: a sufficiently natural extension of arithmetic with logic was found that removes this limitation.
The next major step in the development of sequent calculi was Oiva Ketonen's (1913—2000) 1944 construction of a calculus for classical logic in which all inference rules are invertible; at the same time Ketonen proposed a decomposition approach to proof search that exploits this invertibility property . The axiom-free calculus published in 1949 in the dissertation of Roman Suszko (1919—1979) was close in form to Hertz's constructions, becoming the first embodiment of Hertz-type sequent systems.
In 1952, Stephen Kleene, in “Introduction to Metamathematics,” building on Ketonen's calculus, constructed an intuitionistic sequent calculus with invertible inference rules ; in the same book he also introduced the Gentzen-type calculi 
and 
, which did not require structural[⇨] inference rules, and, overall, after the book's publication, sequent calculi became widely known among specialists .
Starting in the 1950s, the main focus shifted to transferring consistency and completeness results to higher-order predicate calculi, type theories, and non-classical logics. In 1953, Gaisi Takeuti (Jap. 竹内外史; 1926—2017) constructed a sequent calculus for simple type theory, which expresses higher-order predicate calculi, and conjectured that cut elimination holds for it (the Takeuti conjecture). In 1966, William Tait (b. 1929) proved cut elimination for second-order logic; the conjecture was soon proved in full in the work of Motoo Takahashi[10] and Dag Prawitz (b. 1936). In the 1970s the results were substantially extended: Dragalin found proofs of cut elimination for a series of higher-order non-classical logics, and Girard[fr] did so for system F.
Starting in the 1980s, sequent systems have played a key role in the development of automated proof systems; in particular, the sequent Calculus of Constructions developed by Thierry Coquand and Gérard Huet in 1986 — a polymorphic higher-order λ-calculus with dependent types, occupying the top point of Barendregt's λ-cube is used as the basis of the Coq software system.
The most commonly used sequent calculus for classical predicate calculus is the system , constructed by Gentzen in 1934. The system has a single axiom scheme — — and 21 inference rules, which are divided into structural and logical ones[11].
Structural rules (, 
are formulas; , , 
, 
are lists of formulas):
and on the right: 
;
and on the right: 
;
and on the right: 
,
.The logical propositional rules are intended for introducing propositional connectives into the derivation:
-left: 
; -right: 
;
-left: 
and 
; -right: 
,
-left: 
; -right: 
and 
,
-left: 
and -right: 
.The logical quantifier rules introduce the universal and existential quantifiers into the derivation (
is a formula with a free variable 
, 
is an arbitrary term, and 
is the replacement of every occurrence of the free variable with the term ):
-left: 
and -right: 
;
-left: 
and -right: 
.An additional condition in the quantifier rules is that the free variable must not occur in the lower sequent formulas of the rules -right and -left.
An example of an -derivation of the law of excluded middle:
— here the derivation starts from a single axiom, after which the rules -right, -right, exchange on the right, -right, and contraction on the right are applied in sequence.
The calculus is equivalent to first-order classical predicate calculus: a formula is valid in predicate calculus if and only if, in , the sequent 
is derivable. The key result, which Gentzen called the “Hauptsatz” (main theorem), is that any -derivation can be carried out without using the cut rule; it is precisely this property that establishes all the main properties of , including soundness, consistency, and completeness.
The calculus is obtained from by adding a restriction on the succedents of sequents in the inference rules: only a single formula may be used in them, and the rules of exchange on the right and contraction on the right (which operate on several formulas in the succedent) are excluded. Thus, with minimal modifications, a system is obtained in which the laws of double negation and excluded middle are not derivable, but all the other basic logical laws hold, and, for example, the equivalence 
is derivable. The resulting system is equivalent to intuitionistic predicate calculus with Heyting's axioms. In the calculus , cut is also eliminable; it is likewise sound, consistent, and complete, and this last result for intuitionistic predicate calculus was in fact first obtained precisely for .
A large number of variants of sequent calculi for classical and intuitionistic logic have been created, equivalent to one another but convenient for one purpose or another. Some of these calculi inherit Gentzen's construction used in the proof of the consistency of Peano arithmetic and include elements of natural-deduction systems; among these is the 1957 system of Suppes (Patrick Suppes; 1922—2014)[12] (drawn from remarks by Feys[en] and Ladrière[fr] on the French translation of Gentzen's paper), and its improved version, published in 1965 by Lemmon (John Lemmon; 1930—1966)[13], which eliminate the practical inconveniences of using Gentzen's original natural-sequent style[14]. More radical improvements for the practical convenience of natural-style derivation in sequent calculi were proposed by Hermes (Hans Hermes; 1912—2003)[15]: in his system for classical logic two axioms are used ( and 
, while in the inference rules propositional connectives are used not only in succedents but also in antecedents, both in the lower and in the upper sequents[16].
Sequent calculi possess a symmetry that naturally expresses the duality that, in axiomatic theories, is formulated via De Morgan's laws
Comments