In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the natural style of deduction used by mathematicians than David Hilbert's earlier style of formal logic, in which every line was an unconditional tautology. More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical axioms. In that case, sequents signify conditional theorems of a first-order theory rather than conditional tautologies.
Sequent calculus is one of several extant styles of proof calculus for expressing line-by-line logical arguments. Hilbert style. Every line is an unconditional tautology (or theorem). Gentzen style. Every line is a conditional tautology (or theorem) with zero or more conditions on the left. Natural deduction. Every (conditional) line has exactly one asserted proposition on the right. Sequent calculus. Every (conditional) line has zero or more asserted propositions on the right. In other words, natural deduction and sequent calculus systems are particular distinct kinds of Gentzen-style systems. Hilbert-style systems typically have a very small number of inference rules, relying more on sets of axioms. Gentzen-style systems typically have very few axioms, if any, relying more on sets of rules.
Gentzen-style systems have significant practical and theoretical advantages compared to Hilbert-style systems. For example, both natural deduction and sequent calculus systems facilitate the elimination and introduction of universal and existential quantifiers so that unquantified logical expressions can be manipulated according to the much simpler rules of propositional calculus. In a typical argument, quantifiers are eliminated, then propositional calculus is applied to unquantified expressions (which typically contain free variables), and then the quantifiers are reintroduced. This very much parallels the way in which mathematical proofs are carried out in practice by mathematicians. Predicate calculus proofs are generally much easier to discover with this approach, and are often shorter. Natural deduction systems are more suited to practical theorem-proving. Sequent calculus systems are more suited to theoretical analysis.
Overview
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi systems, LK and LJ, were introduced in 1934/1935 by Gerhard Gentzen, . as a tool for studying natural deduction in first-order logic (in classical and intuitionistic versions, respectively). Gentzen's so-called "Main Theorem" (Hauptsatz) about LK and LJ was the cut-elimination theorem,, gives a 5-page proof of the elimination theorem. See also pages 188, 250., gives a very brief proof of the cut-elimination theorem. a result with far-reaching meta-theoretic consequences, including consistency. Gentzen further demonstrated the power and flexibility of this technique a few years later, applying a cut-elimination argument to give a (transfinite) proof of the consistency of Peano arithmetic, in surprising response to Gödel's incompleteness theorems. Since this early work, sequent calculi, also called Gentzen systems,, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.. This book is much more concerned with the theoretical, metamathematical implications of Gentzen-style sequent calculus than applications to practical logic proofs., defines Gentzen systems and proves various theorems within these systems, including Gödel's completeness theorem and Gentzen's theorem., gives a brief theoretical presentation of Gentzen systems. He uses the tableau proof layout style. and the general concepts relating to them, have been widely applied in the fields of proof theory, mathematical logic, and automated deduction.
Hilbert-style deduction systems
One way to classify different styles of deduction systems is to look at the form of judgments in the system, i.e., which things may appear as the conclusion of a (sub)proof. The simplest judgment form is used in Hilbert-style deduction systems, where a judgment has the form
where is any formula of first-order logic (or whatever logic the deduction system applies to, e.g., propositional calculus or a higher-order logic or a modal logic). The theorems are those formulas that appear as the concluding judgment in a valid proof. A Hilbert-style system needs no distinction between formulas and judgments; we make one here solely for comparison with the cases that follow.
The price paid for the simple syntax of a Hilbert-style system is that complete formal proofs tend to get extremely long. Concrete arguments about proofs in such a system almost always appeal to the deduction theorem. This leads to the idea of including the deduction theorem as a formal rule in the system, which happens in natural deduction.
Natural deduction systems
In natural deduction, judgments have the shape
where the 's and are again formulas and . In other words, a judgment consists of a list (possibly empty) of formulas on the left-hand side of a turnstile symbol "", with a single formula on the right-hand side,, compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical., is an introductory presentation of practical natural deduction of this kind. This became the basis of System L. is an elementary introduction to practical natural deduction based on the convenient abbreviated proof layout style System L based on . (though permutations of the 's are often immaterial). The theorems are those formulae such that (with an empty left-hand side) is the conclusion of a valid proof. (In some presentations of natural deduction, the s and the turnstile are not written down explicitly; instead a two-dimensional notation from which they can be inferred is used.)
The standard semantics of a judgment in natural deduction is that it asserts that wheneverHere, "whenever" is used as an informal abbreviation "for every assignment of values to the free variables in the judgment" , , etc., are all true, will also be true. The judgments
and
are equivalent in the strong sense that a proof of either one may be extended to a proof of the other.
Sequent calculus systems
Finally, sequent calculus generalizes the form of a natural deduction judgment to
a syntactic object called a sequent. The formulas on left-hand side of the turnstile are called the antecedent, and the formulas on right-hand side are called the succedent or consequent; together they are called cedents or sequent formulas. Again, and are formulas, and and are nonnegative integers, that is, the left-hand-side or the right-hand-side (or neither or both) may be empty. As in natural deduction, theorems are those where is the conclusion of a valid proof.
The standard semantics of a sequent is an assertion that whenever every is true, at least one will also be true.For explanations of the disjunctive semantics for the right side of sequents, see , , , , and . Thus the empty sequent, having both cedents empty, is false. One way to express this is that a comma to the left of the turnstile should be thought of as an "and", and a comma to the right of the turnstile should be thought of as an (inclusive) "or". The sequents
and
are equivalent in the strong sense that a proof of either sequent may be extended to a proof of the other sequent.
At first sight, this extension of the judgment form may appear to be a strange complication—it is not motivated by an obvious shortcoming of natural deduction, and it is initially confusing that the comma seems to mean entirely different things on the two sides of the turnstile. However, in a classical context the semantics of the sequent can also (by propositional tautology) be expressed either as
(at least one of the As is false, or one of the Bs is true) or as
(it cannot be the case that all of the As are true and all of the Bs are false).
In these formulations, the only difference between formulas on either side of the turnstile is that one side is negated. Thus, swapping left for right in a sequent corresponds to negating all of the constituent formulas. This means that a symmetry such as De Morgan's laws, which manifests itself as logical negation on the semantic level, translates directly into a left–right symmetry of sequents—and indeed, the inference rules in sequent calculus for dealing with conjunction (∧) are mirror images of those dealing with disjunction (∨).
Many logicians feel that this symmetric presentation offers a deeper insight in the structure of the logic than other styles of proof system, where the classical duality of negation is not as apparent in the rules., explore how sequent calculus, particularly in focused proof systems, reveals computational structure through the duality of call-by-name and call-by-value. They argue that the symmetry in sequent calculus—especially when focusing is applied—exposes a deep computational duality and clarifies the structure of proofs and programs in a way that natural deduction does not., highlight the symmetry of the sequent calculus as a foundational motivation for their work. They describe the sequent calculus as “a proof system which was designed as a more symmetric alternative to natural deduction.”
Distinction between natural deduction and sequent calculus
Gentzen asserted a sharp distinction between his single-output natural deduction systems (NK and NJ) and his multiple-output sequent calculus systems (LK and LJ). He wrote that the intuitionistic natural deduction system NJ was somewhat ugly.. "Der Kalkül NJ hat manche formale Unschönheiten." He said that the special role of the excluded middle in the classical natural deduction system NK is removed in the classical sequent calculus system LK.. "In dem klassischen Kalkül NK nahm der Satz vom ausgeschlossenen Dritten eine Sonderstellung unter den Schlußweisen ein [...], indem er sich der Einführungs- und Beseitigungssystematik nicht einfügte. Bei dem im folgenden anzugebenden logistischen klassichen Kalkül LK wird diese Sonderstellung aufgehoben." He said that the sequent calculus LJ gave more symmetry than natural deduction NJ in the case of intuitionistic logic, as also in the case of classical logic (LK versus NK).. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener." Then he said that in addition to these reasons, the sequent calculus with multiple succedent formulas is intended particularly for his principal theorem ("Hauptsatz").. "Hiermit haben wir einige Gesichtspunkte zur Begründung der Aufstellung der folgenden Kalküle angegeben. Im wesentlichen ist ihre Form jedoch durch die Rücksicht auf den nachher zu beweisenden 'Hauptsatz' bestimmt und kann daher vorläufig nicht näher begründet werden."
Historical notes
The word "sequent" is taken from the word "Sequenz" in Gentzen's 1934 paper. Kleene makes the following comment on the translation into English: "Gentzen says 'Sequenz', which we translate as 'sequent', because we have already used 'sequence' for any succession of objects, where the German is 'Folge'."