Editing Sequent calculus (section)

==Overview<!--'Gentzen system' and 'Gentzen systems' redirect here-->==

In [[proof theory]] and [[mathematical logic]], sequent calculus is a family of [[formal system]]s 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<ref name=gentzen19341935>{{harvnb|Gentzen|1934}}, {{harvnb|Gentzen|1935}}.</ref> as a tool for studying [[natural deduction]] in [[first-order logic]] (in [[Classical logic|classical]] and [[Intuitionistic logic|intuitionistic]] versions, respectively).  Gentzen's so-called "Main Theorem" (''Hauptsatz'') about LK and LJ was the [[cut-elimination theorem]],<ref name=curry_cut_elimination>{{harvnb|Curry|1977|pp=208–213}}, gives a 5-page proof of the elimination theorem. See also pages 188, 250.</ref><ref name=kleene_cut_elimination>{{harvnb|Kleene|2009|pp=453}}, gives a very brief proof of the cut-elimination theorem.</ref> a result with far-reaching [[Metatheory|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) [[Gentzen's consistency proof|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'''<!--boldface per WP:R#PLA-->,<ref>{{harvnb|Curry|1977|pp=189–244}}, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.</ref><ref>{{harvnb|Kleene|2009|pp=440–516}}. This book is much more concerned with the theoretical, metamathematical implications of Gentzen-style sequent calculus than applications to practical logic proofs.</ref><ref>{{harvnb|Kleene|2002|pp=283–312, 331–361}}, defines Gentzen systems and proves various theorems within these systems, including Gödel's completeness theorem and Gentzen's theorem.</ref><ref>{{harvnb|Smullyan|1995|pp=101–127}}, gives a brief theoretical presentation of Gentzen systems. He uses the tableau proof layout style.</ref> 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===
{{Main|Hilbert system}}
One way to classify different styles of deduction systems is to look at the form of ''[[Judgment (mathematical logic)|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 system|Hilbert-style deduction systems]], where a judgment has the form
:<math>B</math>
where <math>B</math> is any [[Well-formed formula|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===
{{Main|Natural deduction}}
In natural deduction, judgments have the shape
:<math>A_1, A_2, \ldots, A_n \vdash B</math>
where the <math>A_i</math>'s and <math>B</math> are again formulas and <math>n\geq 0</math>. In other words, a judgment consists of a ''list'' (possibly empty) of formulas on the left-hand side of a [[Turnstile (symbol)|turnstile]] symbol "<math>\vdash</math>", with a single formula on the right-hand side,<ref>{{harvnb|Curry|1977|pp=184–244}}, compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical.</ref><ref>{{harvnb|Suppes|1999|pp=25–150}}, is an introductory presentation of practical natural deduction of this kind. This became the basis of [[System L]].</ref><ref>{{harvnb|Lemmon|1965}} is an elementary introduction to practical natural deduction based on the convenient abbreviated proof layout style [[System L]] based on {{harvnb|Suppes|1999|pp=25–150}}.</ref> (though permutations of the <math>A_i</math>'s are often immaterial). The theorems are those formulae <math>B</math> such that <math>\vdash B</math> (with an empty left-hand side) is the conclusion of a valid proof.
(In some presentations of natural deduction, the <math>A_i</math>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 whenever<ref>Here, "whenever" is used as an informal abbreviation "for every assignment of values to the free variables in the judgment"</ref> <math>A_1</math>, <math>A_2</math>, etc., are all true, <math>B</math> will also be true. The judgments
:<math>A_1, \ldots, A_n \vdash B</math>
and
:<math>\vdash (A_1 \land \cdots \land A_n) \rightarrow B</math>
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
: <math>A_1, \ldots, A_n \vdash B_1, \ldots, B_k,</math>
a syntactic object called a sequent. The formulas on left-hand side of the [[Turnstile (symbol)|turnstile]] are called the ''antecedent'', and the formulas on right-hand side are called the ''succedent'' or ''consequent''; together they are called ''cedents'' or ''sequents''.{{sfn|Shankar|Owre|Rushby|Stringer-Calvert|2020}} Again, <math>A_i</math> and <math>B_i</math> are formulas, and <math>n</math> and <math>k</math> 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 <math>B</math> where <math>\vdash B</math> is the conclusion of a valid proof.

The standard semantics of a sequent is an assertion that whenever ''every''  <math> A_i</math> is true, ''at least one'' <math>B_i</math> will also be true.<ref>For explanations of the disjunctive semantics for the right side of sequents, see {{harvnb|Curry|1977|pp=189–190}}, {{harvnb|Kleene|2002|pp=290, 297}}, {{harvnb|Kleene|2009|p=441}}, {{harvnb|Hilbert|Bernays|1970|p=385}}, {{harvnb|Smullyan|1995|pp=104–105}} and {{harvnb|Gentzen|1934|p=180}}.</ref> Thus the empty sequent, having both cedents empty, is false.{{sfn|Buss|1998|p=10}} 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
:<math>A_1, \ldots, A_n \vdash B_1, \ldots, B_k</math>
and
:<math>\vdash (A_1 \land\cdots\land A_n)\rightarrow(B_1 \lor\cdots\lor B_k)</math>
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 logic|classical context]] the semantics of the sequent can also (by propositional tautology) be expressed either as
:: <math>\vdash \neg A_1 \lor \neg A_2 \lor \cdots \lor \neg A_n \lor B_1 \lor B_2 \lor\cdots\lor B_k</math>
(at least one of the As is false, or one of the Bs is true) 
:or as
:: <math>\vdash \neg(A_1 \land A_2 \land \cdots \land A_n \land \neg B_1 \land \neg B_2 \land\cdots\land \neg B_k)</math>
(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 {{Citation needed|date=November 2018}} 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.

===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.<ref>{{harvnb|Gentzen|1934|p=188}}. "Der Kalkül ''NJ'' hat manche formale Unschönheiten."</ref> He said that the special role of the [[law of excluded middle|excluded middle]] in the classical natural deduction system NK is removed in the classical sequent calculus system LK.<ref>{{harvnb|Gentzen|1934|p=191}}. "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."</ref> 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).<ref>{{harvnb|Gentzen|1934|p=191}}. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener."</ref> Then he said that in addition to these reasons, the sequent calculus with multiple succedent formulas is intended particularly for his principal theorem ("Hauptsatz").<ref>{{harvnb|Gentzen|1934|p=191}}. "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."</ref>

===Origin of word "sequent"===

The word "sequent" is taken from the word "Sequenz" in Gentzen's 1934 paper.<ref name=gentzen19341935 /> [[Stephen Cole Kleene|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'."{{sfn|Kleene|2002|p=441}}