Vero - Wikipedia - User contributions [en]

Sequent calculus

2025-10-28T17:53:11Z

2A02:1812:110C:DC00:FD52:FD63:CF55:6615:

{{Short description|Style of formal logical argumentation}}
{{use dmy dates|date=March 2025}}
In [[mathematical logic]], '''sequent calculus''' is a style of formal logical [[argument]]ation in which every line of a [[formal proof|proof]] is a conditional [[tautology (logic)|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|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 [[axiom]]s. In that case, sequents signify conditional [[theorem]]s 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 system|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 rule]]s, 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 [[Quantification (logic)|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 variable]]s), 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 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 induction|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''',<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 ''sequent formulas''.{{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 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.<ref>{{harvnb|Curien|Munch-Maccagnoni|2010}}, 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.</ref><ref>{{harvnb|Binder|Tzschentke|Müller|Ostermann|2024}}, 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.”</ref>

===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}}

== Proving logical formulas ==
[[File:Sequent calculus proof tree example.png|thumb|A rooted tree describing a proof finding procedure by sequent calculus]]

=== Reduction trees ===
Sequent calculus can be seen as a tool for proving formulas in [[propositional logic]], similar to the [[method of analytic tableaux]]. It gives a series of steps that allows one to reduce the problem of proving a logical formula to simpler and simpler formulas until one arrives at trivial ones.{{sfn|Kreitz|Constable|2009}}

Consider the following formula:
:<math>((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)</math>

This is written in the following form, where the proposition that needs to be proven is to the right of the [[Turnstile (symbol)|turnstile symbol]] <math>\vdash</math>:
:<math>\vdash((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)</math>

Now, instead of proving this from the axioms, it is enough to assume the premise of the [[Logical consequence|implication]] and then try to prove its conclusion.<ref name=Wadler>"Remember, the way that you [[Proof (truth)|prove]] an [[logical consequence|implication]] is by assuming the [[hypothesis]]."—[[Philip Wadler]], [https://www.youtube.com/watch?v=OGF-TGd-CIo&list=PLWbHc_FXPo2jB6IZ887vLXsPoympL3KEy&index=11 on 2 November 2015, in his Keynote: "Propositions as Types". Minute 14:36 /55:28 of Code Mesh video clip ]</ref> Hence one moves to the following sequent:
:<math>(p\rightarrow r)\lor (q\rightarrow r)\vdash (p\land q)\rightarrow r</math>

Again the right hand side includes an implication, whose premise can further be assumed so that only its conclusion needs to be proven:
:<math>(p\rightarrow r)\lor (q\rightarrow r), (p\land q)\vdash r</math>

Since the arguments in the left-hand side are assumed to be related by [[Logical conjunction|conjunction]], this can be replaced by the following:
:<math>(p\rightarrow r)\lor (q\rightarrow r), p, q\vdash r</math>

This is equivalent to proving the conclusion in both cases of the [[Logical disjunction|disjunction]] on the first argument on the left. Thus we may split the sequent to two, where we now have to prove each separately:
:<math>p\rightarrow r, p, q\vdash r</math>
:<math>q\rightarrow r, p, q\vdash r</math>

In the case of the first judgment, we rewrite <math>p\rightarrow r</math> as <math>\lnot p \lor r</math> and split the sequent again to get:
:<math>\lnot p, p, q \vdash r</math>
:<math>r, p, q \vdash r</math>

The second sequent is done; the first sequent can be further simplified into:
:<math>p, q \vdash p, r</math>

This process can always be continued until there are only atomic formulas in each side.
The process can be graphically described by a [[Tree (graph theory)|rooted tree]], as depicted on the right. The root of the tree is the formula we wish to prove; the leaves consist of atomic formulas only. The tree is known as a '''reduction tree'''.{{sfn|Kreitz|Constable|2009}}{{sfn|Tait|2010}}

The items to the left of the turnstile are understood to be connected by conjunction, and those to the right by disjunction. Therefore, when both consist only of atomic symbols, the sequent is accepted axiomatically (and always true) if and only if at least one of the symbols on the right also appears on the left.

Following are the rules by which one proceeds along the tree. Whenever one sequent is split into two, the tree vertex has two child vertices, and the tree is branched. Additionally, one may freely change the order of the arguments in each side; Γ and Δ stand for possible additional arguments.{{sfn|Kreitz|Constable|2009}}

The usual term for the horizontal line used in Gentzen-style layouts for natural deduction is '''inference line'''.{{sfn|von Plato|2014|page=32}}

{| class="wikitable"
|-
! Left
! Right
|-
| <math>L\land \text{rule: }\quad\cfrac{\Gamma, A \land B\vdash \Delta} {\Gamma, A, B \vdash \Delta}
</math>
| <math>R\land \text{rule: }\cfrac{\Gamma\vdash \Delta, A \land B} {\Gamma \vdash \Delta, A \qquad \Gamma \vdash \Delta, B}
</math>
|-
| <math>L\lor \text{rule: }\cfrac{\Gamma, A \lor B\vdash \Delta} {\Gamma, A \vdash \Delta \qquad \Gamma, B \vdash \Delta}
</math>
| <math>R\lor \text{rule: }\quad\cfrac{\Gamma\vdash \Delta, A \lor B} {\Gamma \vdash \Delta, A, B}
</math>
|-
| <math>L\rightarrow \text{rule: }\cfrac{\Gamma, A \rightarrow B\vdash \Delta} {\Gamma \vdash \Delta,A \qquad \Gamma, B \vdash \Delta}
</math>
| <math>R\rightarrow \text{rule: }\quad\cfrac{\Gamma\vdash \Delta, A \rightarrow B} {\Gamma, A \vdash \Delta, B}
</math>
|-
| <math>L\lnot \text{rule: }\quad\cfrac{\Gamma, \lnot A \vdash \Delta} {\Gamma \vdash \Delta,A }
</math>
| <math>R\lnot \text{rule: }\quad\cfrac{\Gamma\vdash \Delta, \lnot A} {\Gamma, A \vdash \Delta}
</math>
|-
| colspan="2" | Axiom: <math> \Gamma,A \vdash \Delta, A </math>
|}

Starting with any formula in propositional logic, by a series of steps, the right side of the turnstile can be processed until it includes only atomic symbols. Then, the same is done for the left side. Since every logical operator appears in one of the rules above, and is removed by the rule, the process terminates when no logical operators remain: The formula has been ''decomposed''.

Thus, the sequents in the leaves of the trees include only atomic symbols, which are either provable by the axiom or not, according to whether one of the symbols on the right also appears on the left.

It is easy to see that the steps in the tree preserve the semantic truth value of the formulas implied by them, with conjunction understood between the tree's different branches whenever there is a split. It is also obvious that an axiom is provable if and only if it is true for every assignment of truth values to the atomic symbols. Thus this system is [[soundness|sound]] and [[completeness (logic)|complete]] for classical propositional logic.

=== Relation to standard axiomatizations ===

Sequent calculus is related to other axiomatizations of classical propositional calculus, such as Frege's propositional calculus or [[Propositional_calculus#Łukasiewicz's_P2|Jan Łukasiewicz's axiomatization]] (itself a part of the standard [[Hilbert system]]): Every formula that can be proven in these has a reduction tree. This can be shown as follows: Every proof in propositional calculus uses only axioms and the inference rules. Each use of an axiom scheme yields a true logical formula, and can thus be proven in sequent calculus; examples for these are [[Sequent calculus#Example derivations|shown below]]. The only inference rule in the systems mentioned above is [[modus ponens]], which is implemented by the [[cut rule]].

==The system LK==

This section introduces the rules of the sequent calculus '''LK''' (standing for Logistische Kalkül) as introduced by Gentzen in 1934.{{sfn|Indrzejczak|2021|pp=63–112}} A (formal) proof in this calculus is a finite [[sequence (mathematics)|sequence]] of sequents, where each of the sequents is derivable from sequents appearing earlier in the sequence by using one of the [[rule of inference|rules]] below.

===Inference rules===

The following notation will be used:
* <math>\vdash</math> known as the [[Turnstile (symbol)|turnstile]], separates the ''assumptions'' on the left from the ''propositions'' on the right
* <math>A</math> and <math>B</math> denote formulas of first-order predicate logic (one may also restrict this to propositional logic),
* <math>\Gamma, \Delta, \Sigma</math>, and <math>\Pi</math> are finite (possibly empty) sequences of formulas (in fact, the order of formulas does not matter; see {{slink||Structural rules}}), called contexts,
** when on the ''left'' of the <math>\vdash</math>, the sequence of formulas is considered ''conjunctively'' (all assumed to hold at the same time),
** while on the ''right'' of the <math>\vdash</math>, the sequence of formulas is considered ''disjunctively'' (at least one of the formulas must hold for any assignment of variables),
* <math>t</math> denotes an arbitrary term,
* <math>x</math> and <math>y</math> denote variables.
* a variable is said to occur [[Free variables and bound variables|free]] within a formula if it is not bound by quantifiers <math>\forall</math> or <math>\exists</math>.
* <math>A[t/x]</math> denotes the formula that is obtained by substituting the term <math>t</math> for every free occurrence of the variable <math>x</math> in formula <math>A</math> with the restriction that the term <math>t</math> must be free for the variable <math>x</math> in <math>A</math> (i.e., no occurrence of any variable in <math>t</math> becomes bound in <math>A[t/x]</math>).
* <math>WL</math>, <math>WR</math>, <math>CL</math>, <math>CR</math>, <math>PL</math>, <math>PR</math>: These six stand for the two versions of each of three structural rules; one for use on the left ('L') of a <math>\vdash</math>, and the other on its right ('R'). The rules are abbreviated 'W' for ''Weakening (Left/Right)'', 'C' for ''Contraction'', and 'P' for ''Permutation''.

Note that, contrary to the rules for proceeding along the reduction tree presented above, the following rules are for moving in the opposite directions, from axioms to theorems. Thus they are exact mirror-images of the rules above, except that here symmetry is not implicitly assumed, and rules regarding [[quantifier (logic)|quantification]] are added.

In the table below, <math>A \setminus B</math> denotes the [[relative complement]] of <math>B</math> in <math>A</math>.

{| class="wikitable"
|-
! Axiom
! Cut
|-
| <math> \cfrac{\qquad }{ A \vdash A} \quad (I) </math>
| <math>
\cfrac{\Gamma \vdash \Delta, A \qquad A, \Sigma \vdash \Pi} {\Gamma, \Sigma \vdash \Delta, \Pi} \quad (\mathit{Cut})
</math>
|}
{| class="wikitable"
|-
! Left logical rules
! Right logical rules
|-
| <math> \cfrac{\Gamma, A \vdash \Delta} {\Gamma, A \land B \vdash \Delta} \quad ({\land}L_1)
</math>
| <math> \cfrac{\Gamma \vdash A, \Delta}{\Gamma \vdash A \lor B, \Delta} \quad ({\lor}R_1)
</math>
|-
| <math> \cfrac{\Gamma, B \vdash \Delta}{\Gamma, A \land B \vdash \Delta} \quad ({\land}L_2)
</math>
| <math> \cfrac{\Gamma \vdash B, \Delta}{\Gamma \vdash A \lor B, \Delta} \quad ({\lor}R_2)
</math>
|-
| <math> \cfrac{\Gamma, A \vdash \Delta \qquad \Gamma, B \vdash \Delta}{\Gamma, A \lor B \vdash \Delta} \quad ({\lor}L)
</math>
| <math> \cfrac{\Gamma \vdash A, \Delta \qquad \Gamma \vdash B, \Delta}{\Gamma \vdash A \land B, \Delta} \quad ({\land}R)
</math>
|-
| <math>
\cfrac{\Gamma \vdash A, \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A\rightarrow B \vdash \Delta, \Pi} \quad ({\rightarrow }L)
</math>
| <math>
\cfrac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \rightarrow B, \Delta} \quad ({\rightarrow}R)
</math>
|-
| <math>
\cfrac{\Gamma, A \vdash B, \Delta}{\Gamma, A \setminus B \vdash \Delta} \quad ({\setminus}L)
</math>
| <math>
\cfrac{\Gamma \vdash A, \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma \vdash A\setminus B, \Delta, \Pi} \quad ({\setminus }R)
</math>
|-
| <math>
\cfrac{\Gamma \vdash A, \Delta}{\Gamma, \lnot A \vdash \Delta} \quad ({\lnot}L)
</math>
| <math>
\cfrac{\Gamma, A \vdash \Delta}{\Gamma \vdash \lnot A, \Delta} \quad ({\lnot}R)
</math>
|-
| <math>
\cfrac{\Gamma, A[t/x] \vdash \Delta}{\Gamma, \forall x A \vdash \Delta} \quad ({\forall}L)
</math>
| <math>
\cfrac{\Gamma \vdash A[y/x], \Delta}{\Gamma \vdash \forall x A, \Delta} \quad ({\forall}R)
</math> (†)
|-
| <math>
\cfrac{\Gamma, A[y/x] \vdash \Delta}{\Gamma, \exists x A \vdash \Delta} \quad ({\exists}L)
</math> (†)
| <math>
\cfrac{\Gamma \vdash A[t/x], \Delta}{\Gamma \vdash \exists x A, \Delta} \quad ({\exists}R)
</math>
|}
{| class="wikitable"
|-
! Left structural rules
! Right structural rules
|-
| <math>
\cfrac{\Gamma \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{WL})
</math>
| <math>
\cfrac{\Gamma \vdash \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{WR})
</math>
|-
| <math>
\cfrac{\Gamma, A, A \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{CL})
</math>
| <math>
\cfrac{\Gamma \vdash A, A, \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{CR})
</math>
|-
| <math>
\cfrac{\Gamma_1, A, B, \Gamma_2 \vdash \Delta}{\Gamma_1, B, A, \Gamma_2 \vdash \Delta} \quad (\mathit{PL})
</math>
| <math>
\cfrac{\Gamma \vdash \Delta_1, A, B, \Delta_2}{\Gamma \vdash \Delta_1, B, A, \Delta_2} \quad (\mathit{PR})
</math>
|}

'''''Restrictions''': In the rules marked with (†), <math>({\forall}R)</math> and <math>({\exists}L)</math>, the variable <math>y</math> must not occur free anywhere in the respective lower sequents.''

===An intuitive explanation===

The above rules can be divided into two major groups: ''logical'' and ''structural'' ones. Each of the logical rules introduces a new logical formula either on the left or on the right of the [[Turnstile (symbol)|turnstile]] <math>\vdash</math>. In contrast, the structural rules operate on the structure of the sequents, ignoring the exact shape of the formulas. The two exceptions to this general scheme are the axiom of identity (I) and the rule of (Cut).

Although stated in a formal way, the above rules allow for a very intuitive reading in terms of classical logic. Consider, for example, the rule <math>({\land}L_1)</math>. It says that, whenever one can prove that <math>\Delta</math> can be concluded from some sequence of formulas that contain <math>A</math>, then one can also conclude <math>\Delta</math> from the (stronger) assumption that <math>A \land B</math> holds. Likewise, the rule <math>({\neg}R)</math> states that, if <math>\Gamma</math> and <math>A</math> suffice to conclude <math>\Delta</math>, then from <math>\Gamma</math> alone one can either still conclude <math>\Delta</math> or that <math>A</math> must be false, i.e. <math>{\neg}A</math> holds. All the rules can be interpreted in this way.

For an intuition about the quantifier rules, consider the rule <math>({\forall}R)</math>. Of course concluding that <math>\forall{x} A</math> holds just from the fact that <math>A[y/x]</math> is true is not in general possible. If, however, the variable ''y'' is not mentioned elsewhere (i.e. it can still be chosen freely, without influencing the other formulas), then one may assume, that <math>A[y/x]</math> holds for any value of ''y''. The other rules should then be pretty straightforward.

Instead of viewing the rules as descriptions for legal derivations in predicate logic, one may also consider them as instructions for the construction of a proof for a given statement. In this case the rules can be read bottom-up; for example, <math>({\land}R)</math> says that, to prove that <math>A \land B</math> follows from the assumptions <math>\Gamma</math> and <math>\Sigma</math>, it suffices to prove that <math>A</math> can be concluded from <math>\Gamma</math> and <math>B</math> can be concluded from <math>\Sigma</math>, respectively. Note that, given some antecedent, it is not clear how this is to be split into <math>\Gamma</math> and <math>\Sigma</math>. However, there are only finitely many possibilities to be checked since the antecedent by assumption is finite. This also illustrates how proof theory can be viewed as operating on proofs in a combinatorial fashion: given proofs for both <math>A</math> and <math>B</math>, one can construct a proof for <math>A \land B</math>.

When looking for some proof, most of the rules offer more or less direct recipes of how to do this. The rule of cut is different: it states that, when a formula <math>A</math> can be concluded and this formula may also serve as a premise for concluding other statements, then the formula <math>A</math> can be "cut out" and the respective derivations are joined. When constructing a proof bottom-up, this creates the problem of guessing <math>A</math> (since it does not appear at all below). The [[cut-elimination theorem]] is thus crucial to the applications of sequent calculus in [[automated deduction]]: it states that all uses of the cut rule can be eliminated from a proof, implying that any provable sequent can be given a ''cut-free'' proof.

The second rule that is somewhat special is the axiom of identity (I). The intuitive reading of this is obvious: every formula proves itself. Like the cut rule, the axiom of identity is somewhat redundant: the [[completeness of atomic initial sequents]] states that the rule can be restricted to [[atomic formula]]s without any loss of provability.

Observe that, if we ignore the non-standard connective \, all rules have mirror companions, except the ones for implication. This reflects the fact that the usual language of first-order logic does not include the "is not implied by" connective <math>\not\leftarrow</math> that would be the De Morgan dual of implication. Adding such a connective with its natural rules makes the calculus completely left–right symmetric.

===Example derivations===

Here is the derivation of "<math> \vdash A \lor \lnot A </math>", known as
the ''[[Law of excluded middle]]'' (''tertium non datur'' in Latin).
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|  
|  
| rowspan=2 | <math>
(I)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
A \vdash A
</math>
|  
|-
|  
| rowspan=2 | <math>
(\lnot R)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\vdash \lnot A , A
</math>
|  
|-
|  
| rowspan=2 | <math>
(\lor R_2)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\vdash A \lor \lnot A , A
</math>
|  
|-
|  
| rowspan=2 | <math>
(PR)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\vdash A , A \lor \lnot A
</math>
|  
|-
|  
| rowspan=2 | <math>
(\lor R_1)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\vdash A \lor \lnot A , A \lor \lnot A
</math>
|  
|-
|  
| rowspan=2 | <math>
(CR)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\vdash A \lor \lnot A
</math>
|  
|-
|  
|  
|}

Next is the proof of a simple fact involving quantifiers. Note that the converse is not true, and its falsity can be seen when attempting to derive it bottom-up, because an existing free variable cannot be used in substitution in the rules <math>(\forall R)</math> and <math>(\exists L)</math>.
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|  
|  
| rowspan=2 | <math>
(I)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
p(x,y) \vdash p(x,y)
</math>
|  
|-
|  
| rowspan=2 | <math>
(\forall L)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\forall x \left( p(x,y) \right) \vdash p(x,y)
</math>
|  
|-
|  
| rowspan=2 | <math>
(\exists R)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\forall x \left( p(x,y) \right) \vdash \exists y \left( p(x,y) \right)
</math>
|  
|-
|  
| rowspan=2 | <math>
(\exists L)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\exists y \left( \forall x \left( p(x,y) \right) \right) \vdash \exists y \left( p(x,y) \right)
</math>
|  
|-
|  
| rowspan=2 | <math>
(\forall R)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\exists y \left( \forall x \left( p(x,y) \right) \right) \vdash \forall x \left( \exists y \left( p(x,y) \right) \right)
</math>
|  
|-
|  
|  
|}

For something more interesting we shall prove <math>{\left( \left( A \rightarrow \left( B \lor C \right) \right) \rightarrow \left( \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \rightarrow \lnot A \right) \right)}</math>. It is straightforward to find the derivation, which exemplifies the usefulness of LK in automated proving.
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|
{| align=center border=0 cellspacing=0 cellpadding=0
|-
| valign=bottom |
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|  
|  
| rowspan=2 | <math>
(I)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
A \vdash A
</math>
|  
|-
|  
| rowspan=2 | <math>
(\lnot R)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\vdash \lnot A , A
</math>
|  
|-
|  
| rowspan=2 | <math>
(PR)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\vdash A , \lnot A
</math>
|  
|-
|  
|  
|}
|   
| valign=bottom |
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|
{| align=center border=0 cellspacing=0 cellpadding=0
|-
| valign=bottom |
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|
{| align=center border=0 cellspacing=0 cellpadding=0
|-
| valign=bottom |
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|
| |  
| rowspan=2 | <math>
(I)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
B \vdash B
</math>
|  
|-
|  
| rowspan=2 | <math>
(WR)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
B \vdash B, C
</math>
|  
|-
|  
|  
|}
|   
| valign=bottom |
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|
| |  
| rowspan=2 | <math>
(I)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
C \vdash C
</math>
|  
|-
|  
| rowspan=2 | <math>
(WR)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
C \vdash B, C
</math>
|  
|-
|  
|  
|}
|}
|  
| rowspan=2 valign=bottom | <math>
(\lor L)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
B \lor C \vdash B , C
</math>
|  
|-
|  
| rowspan=2 | <math>
(PR)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
B \lor C \vdash C , B
</math>
|  
|-
|  
| rowspan=2 | <math>
(\lnot L)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
B \lor C , \lnot C \vdash B
</math>
|  
|-
|  
|  
|}
|   
| valign=bottom |
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|  
|  
| rowspan=2 | <math>
(I)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\lnot A \vdash \lnot A
</math>
|  
|-
|  
|  
|}
|}
|  
| rowspan=2 valign=bottom | <math>
(\rightarrow L)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\left( B \lor C \right) , \lnot C , \left( B \rightarrow \lnot A \right) \vdash \lnot A
</math>
|  
|-
|  
| rowspan=2 | <math>
(\land L_1)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\left( B \lor C \right) , \lnot C , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \vdash \lnot A
</math>
|  
|-
|  
| rowspan=2 | <math>
(PL)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\left( B \lor C \right) , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) , \lnot C \vdash \lnot A
</math>
|  
|-
|  
| rowspan=2 | <math>
(\land L_2)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\left( B \lor C \right) , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \vdash \lnot A
</math>
|  
|-
|  
| rowspan=2 | <math>
(CL)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\left( B \lor C \right) , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \vdash \lnot A
</math>
|  
|-
|  
| rowspan=2 | <math>
(PL)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) , \left( B \lor C \right) \vdash \lnot A
</math>
|  
|-
|  
|  
|}
|}
|  
| rowspan=2 valign=bottom | <math>
(\rightarrow L)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) , \left( A \rightarrow \left( B \lor C \right) \right) \vdash \lnot A , \lnot A
</math>
|  
|-
|  
| rowspan=2 | <math>
(CR)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) , \left( A \rightarrow \left( B \lor C \right) \right) \vdash \lnot A
</math>
|  
|-
|  
| rowspan=2 | <math>
(PL)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\left( A \rightarrow \left( B \lor C \right) \right) , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \vdash \lnot A
</math>
|  
|-
|  
| rowspan=2 | <math>
(\rightarrow R)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\left( A \rightarrow \left( B \lor C \right) \right) \vdash \left( \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \rightarrow \lnot A \right)
</math>
|  
|-
|  
| rowspan=2 | <math>
(\rightarrow R)
</math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
\vdash \left( \left( A \rightarrow \left( B \lor C \right) \right) \rightarrow \left( \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \rightarrow \lnot A \right) \right)
</math>
|  
|-
|  
|  
|}

These derivations also emphasize the strictly formal structure of the sequent calculus. For example, the logical rules as defined above always act on a formula immediately adjacent to the turnstile, such that the permutation rules are necessary. Note, however, that this is in part an artifact of the presentation, in the original style of Gentzen. A common simplification involves the use of [[multiset]]s of formulas in the interpretation of the sequent, rather than sequences, eliminating the need for an explicit permutation rule. This corresponds to shifting commutativity of assumptions and derivations outside the sequent calculus, whereas LK embeds it within the system itself.

===Relation to analytic tableaux===
For certain formulations (i.e. variants) of the sequent calculus, a proof in such a calculus is isomorphic to an upside-down, closed [[method of analytic tableaux|analytic tableau]].<ref>{{harvnb|Smullyan|1995|p=107}}</ref>

===Structural rules===

The structural rules deserve some additional discussion.

Weakening (W) allows the addition of arbitrary elements to a sequence. Intuitively, this is allowed in the antecedent because we can always restrict the scope of our proof (if all cars have wheels, then it's safe to say that all black cars have wheels); and in the succedent because we can always allow for alternative conclusions (if all cars have wheels, then it's safe to say that all cars have either wheels or wings).

Contraction (C) and Permutation (P) assure that neither the order (P) nor the multiplicity of occurrences (C) of elements of the sequences matters. Thus, one could instead of [[sequence]]s also consider [[Set (mathematics)|sets]].

The extra effort of using sequences, however, is justified since part or all of the structural rules may be omitted. Doing so, one obtains the so-called [[substructural logic]]s.

===Properties of the system LK===

This system of rules can be shown to be both [[soundness|sound]] and [[completeness (logic)|complete]] with respect to first-order logic, i.e. a statement <math>A</math> follows [[semantics|semantically]] from a set of premises <math>\Gamma</math> <math>(\Gamma \vDash A)</math> [[if and only if]] the sequent <math>\Gamma \vdash A</math> can be derived by the above rules.<ref>{{harvnb|Kleene|2002|p=336}}, wrote in 1967 that "it was a major logical discovery by Gentzen 1934–5 that, when there is any (purely logical) proof of a proposition, there is a direct proof. The implications of this discovery are in theoretical logical investigations, rather than in building collections of proved formulas."</ref>

In the sequent calculus, the rule of [[cut-elimination|cut is admissible]]. This result is also referred to as Gentzen's ''Hauptsatz'' ("Main Theorem").<ref name=curry_cut_elimination /><ref name=kleene_cut_elimination />

==Variants==

The above rules can be modified in various ways:

===Minor structural alternatives===

There is some freedom of choice regarding the technical details of how sequents and structural rules are formalized without changing what sequents the system derives.

First of all, as mentioned above, the sequents can be viewed to consist of sets or [[multiset]]s. In this case, the rules for permuting and (when using sets) contracting formulas are unnecessary.

The rule of weakening becomes [[admissible rule|admissible]] if the axiom (I) is changed to derive any sequent of the form <math>\Gamma , A \vdash A , \Delta</math>. Any weakening that appears in a derivation can then be moved to the beginning of the proof. This may be a convenient change when constructing proofs bottom-up.

One may also change whether rules with more than one premise share the same context for each of those premises or split their contexts between them: For example, <math>({\lor}L)</math> may be instead formulated as

:<math>
\cfrac{\Gamma, A \vdash \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A \lor B \vdash \Delta, \Pi}.
</math>

Contraction and weakening make this version of the rule interderivable with the version above, although in their absence, as in [[linear logic]], these rules define different connectives.

===Absurdity===
One can introduce <math>\bot</math>, the [[principle of explosion|absurdity constant]] representing ''false'', with the axiom:

:<math>
\cfrac{}{\bot \vdash \quad }
</math>

Or if, as described above, weakening is to be an admissible rule, then with the axiom:

:<math>
\cfrac{}{\Gamma, \bot \vdash \Delta}
</math>

With <math>\bot</math>, negation can be subsumed as a special case of implication, via the definition <math>(\neg A) \iff (A \to \bot)</math>.

===Substructural logics===
{{main article|Substructural logic}}

Alternatively, one may restrict or forbid the use of some of the structural rules. This yields a variety of [[substructural logic]] systems. They are generally weaker than LK (''i.e.'', they have fewer theorems), and thus not complete with respect to the standard semantics of first-order logic. However, they have other interesting properties that have led to applications in theoretical [[computer science]] and [[artificial intelligence]].

===Intuitionistic sequent calculus: System LJ===

Surprisingly, some small changes in the rules of LK suffice to turn it into a proof system for [[intuitionistic logic]].<ref>{{harvnb|Gentzen|1934|p=194}}, wrote: "Der Unterschied zwischen ''intuitionistischer'' und ''klassischer'' Logik ist bei den Kalkülen ''LJ'' und ''LK'' äußerlich ganz anderer Art als bei ''NJ'' und ''NK''. Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Sukzedensbedingung ausgedrückt wird." English translation: "The difference between ''intuitionistic'' and ''classical'' logic is in the case of the calculi ''LJ'' and ''LK'' of an extremely, totally different kind to the case of ''NJ'' and ''NK''. In the latter case, it consisted of the removal or addition respectively of the excluded middle rule, whereas in the former case, it is expressed through the succedent conditions."</ref> To this end, one has to restrict to sequents with at most one formula on the right-hand side,{{sfn|Tiomkin|1988}} and modify the rules to maintain this invariant. For example, <math>({\lor}L)</math> is reformulated as follows (where C is an arbitrary formula):

:<math>
\cfrac{\Gamma, A \vdash C \qquad \Gamma, B \vdash C }{\Gamma, A \lor B \vdash C} \quad ({\lor}L)
</math>

The resulting system is called LJ. It is sound and complete with respect to intuitionistic logic and admits a similar cut-elimination proof. This can be used in proving [[disjunction and existence properties]].

In fact, the only rules in LK that need to be restricted to single-formula consequents are <math>({\to}R)</math>, <math>(\neg R)</math> (which can be seen as a special case of <math>{\to}R</math>, as described above) and <math>({\forall}R)</math>. When multi-formula consequents are interpreted as disjunctions, all of the other inference rules of LK are derivable in LJ, while the rules <math>({\to}R)</math> and <math>({\forall}R)</math> become
:<math>
\cfrac{\Gamma, A \vdash B \lor C}{\Gamma \vdash (A \to B) \lor C}
</math>
and (when <math>y</math> does not occur free in the bottom sequent)
:<math>
\cfrac{\Gamma \vdash A[y/x] \lor C}{\Gamma \vdash (\forall x A) \lor C}.
</math>

These two rules are ''not'' intuitionistically valid.

==See also==
* [[Cirquent calculus]]
* [[Nested sequent calculus]]
* [[Resolution (logic)]]
* [[Proof theory]]

==Notes==
{{Reflist}}

==References==
* {{cite journal |last1=Binder |first1=David |last2=Tzschentke |first2=Marco |last3=Müller |first3=Marius| last4=Ostermann |first4=Klaus |title=Grokking the Sequent Calculus (Functional Pearl) |journal=Proceedings of the ACM on Programming Languages |arxiv=2406.14719 |date=2024-06-20 |volume=8 |pages=395–425 |doi=10.1145/3674639 }}
* {{cite book|last=Buss|first=Samuel R.|authorlink = Samuel R. Buss|chapter=An introduction to proof theory | editor = Samuel R. Buss | title=Handbook of proof theory | pages = 1–78 | url = http://math.ucsd.edu/~sbuss/ResearchWeb/handbookI/ | publisher = Elsevier | year = 1998 | isbn = 0-444-89840-9 }}
* {{cite arXiv |last1=Curien |first1=Pierre-Louis |last2=Munch-Maccagnoni |first2=Guillaume |title=The duality of computation under focus |eprint=1006.2283 |class=cs.LO |date=2010-06-11}}
* {{cite book|last=Curry|first=Haskell Brooks|author-link=Haskell Curry|title=Foundations of mathematical logic|orig-year=1963|year=1977|publisher=Dover Publications Inc.|location=New York|isbn=978-0-486-63462-3}}
* {{Cite journal|last=Gentzen|first=Gerhard Karl Erich|author-link=Gerhard Gentzen|title=Untersuchungen über das logische Schließen. I|journal=[[Mathematische Zeitschrift]]|volume=39|issue=2|year=1934|doi=10.1007/BF01201353|pages=176–210|s2cid=121546341|url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375508|url-access=subscription}}
* {{Cite journal|last=Gentzen|first=Gerhard Karl Erich|author-link=Gerhard Gentzen|title=Untersuchungen über das logische Schließen. II|journal=Mathematische Zeitschrift|volume=39|issue=3|year=1935|pages=405–431|url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375605|doi=10.1007/bf01201363|s2cid=186239837|url-access=subscription}}
* {{cite book | first=Jean-Yves | last=Girard | author-link=Jean-Yves Girard | author2=Paul Taylor | author3=Yves Lafont | title=Proofs and Types | publisher=Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7) | year=1990 | orig-year=1989 | isbn=0-521-37181-3 | url=https://archive.org/details/proofstypes0000gira | url-access=registration }}
* {{cite book|last1=Hilbert|first1=David| author1-link=David Hilbert | last2=Bernays | first2=Paul |author2-link=Paul Bernays|title=Grundlagen der Mathematik II|orig-year=1939|year=1970|publisher=Springer-Verlag|location=Berlin, New York|isbn=978-3-642-86897-9|edition=Second}}
* {{cite book | last=Indrzejczak | first=Andrzej | year=2021 | chapter-url=https://link.springer.com/chapter/10.1007/978-3-030-57145-0_2 | doi=10.1007/978-3-030-57145-0_2 | chapter=Gentzen's Sequent Calculus LK | title=Sequents and Trees {{!}} An Introduction to the Theory and Applications of Propositional Sequent Calculi| series=Studies in Universal Logic | pages=63–112 |publisher= Springer Nature Switzerland AG|location=Cham, Switzerland | isbn=978-3-030-57144-3 }}
* {{cite book|last=Kleene|first=Stephen Cole|author-link=Stephen Cole Kleene|title=Introduction to metamathematics|orig-year=1952|year=2009|publisher=Ishi Press International|isbn=978-0-923891-57-2}}
* {{cite book|last=Kleene|first=Stephen Cole|author-link=Stephen Cole Kleene|title=Mathematical logic|orig-year=1967|year=2002|publisher=Dover Publications|location=Mineola, New York|isbn=978-0-486-42533-7}}
* {{cite book|last=Lemmon|first=Edward John|author-link=John Lemmon|title=Beginning logic|year=1965|publisher=Thomas Nelson|isbn=0-17-712040-1}}
* {{cite web | last1 = Kreitz | first1 = Christoph | last2 = Constable | first2 = Robert | date = 2009-02-17 | title = Applied Logic, Univ. of Cornell: Lecture 9 | url = https://www.cs.cornell.edu/courses/cs4860/2009sp/lec-09.pdf | publisher = Cornell University | access-date = 2025-06-01}}
* {{cite book|last1=Mancosu|first1=Paolo|author1-link=|last2=Galvan|first2=Sergio|author2-link=|last3=Zach|first3=Richard|author3-link=Richard Zach|title=An Introduction to Proof Theory {{mdash}} Normalization, Cut-Elimination, and Consistency Proofs|pages=431|year=2021|publisher=[[Oxford University Press]]|isbn=978-0-19-289593-6}}
*{{cite web |url=http://pvs.csl.sri.com/doc/pvs-prover-guide.pdf |title=PVS Prover Guide |last1=Shankar |first1=Natarajan |author-link=Natarajan Shankar |last2=Owre |first2=Sam |last3=Rushby |first3=John M. |author-link3=John Rushby |last4=Stringer-Calvert |first4=David W. J. |work=User guide |publisher=[[SRI International]] |date=2020|access-date=2025-06-01 }}
* {{cite book|last=Smullyan|first=Raymond Merrill|author-link=Raymond Smullyan|year=1995|orig-year=1968|title=First-order logic|publisher=Dover Publications|location=New York|isbn=978-0-486-68370-6}}
* {{cite book|last=Suppes|first=Patrick Colonel|author-link=Patrick Suppes|year=1999|orig-year=1957|title=Introduction to logic|publisher=Dover Publications|location=Mineola, New York|isbn=978-0-486-40687-9}}
* {{cite book | last = Tait | first = William W. | title = Gentzen's Centenary: The Quest for Consistency | chapter = Gentzen's original consistency proof and the Bar Theorem | chapter-url = https://doi.org/10.1007/978-3-319-10103-3_8 | editor1-last = Kahle | editor1-first = Reinhard | editor2-last = Rathjen | editor2-first = Michael | pages = 213–228 | location = New York | publisher = Springer | year = 2010 | doi = 10.1007/978-3-319-10103-3_8 | isbn = 978-3-319-10102-6}}
*{{cite conference
| last = Tiomkin
| first = M.
| title = Proving unprovability
| book-title = Proceedings of the Third Annual [[Symposium on Logic in Computer Science]], July 5–8, 1988
| year = 1988
| pages = 22–26
| publisher = Computer Society Press
| isbn = 0-8186-0853-6
}}
* {{cite book | last = von Plato | first = Jan |author-link = :de:Jan von Plato|title = Elements of Logical Reasoning | publisher = [[Cambridge University Press]] | year = 2014 | isbn = 9781139567862|doi=10.1017/CBO9781139567862}}

==External links==
*{{cite encyclopedia 
|author-last=Rathjen
|author-first=Michael
|author-last2=Sieg
|author-first2=Wilfried
|date=2024
|url=https://plato.stanford.edu/archives/win2024/entries/proof-theory/#SequCalc
|title=Proof Theory (Sequent Calculi)
|editor-last1=Zalta
|editor-first1=Edward N.
|editor-link1=Edward N. Zalta
|editor-last2=Nodelman
|editor-first2=Uri
|encyclopedia=[[Stanford Encyclopedia of Philosophy]]
|edition=Winter 2024
}}
* {{springer|title=Sequent calculus|id=p/s084580}}
* {{cite web
|url=https://scienceblogs.com/goodmath/2006/07/17/a-brief-diversion-sequent-calc/
|title=A Brief Diversion: Sequent Calculus
|website=Good Math, Bad Math
|date=2 August 2010
|access-date=2025-03-27
}}
* {{cite web
|url=http://logitext.mit.edu/logitext.fcgi/tutorial
|title=Interactive Tutorial of the Sequent Calculus
|website=Logitext (MIT)
|access-date=2025-03-27
}}

[[Category:Proof theory]]
[[Category:Logical calculi]]
[[Category:Automated theorem proving]]
{{Diagrams in logic}}

Noncommutative logic

2025-10-28T17:41:26Z

2A02:1812:110C:DC00:FD52:FD63:CF55:6615:

'''Noncommutative logic''' is an extension of [[linear logic]] that combines the [[commutative]] [[logical connective|connective]]s of linear logic with the noncommutative multiplicative [[connective (logic)|connective]]s of the [[Lambek calculus]]. Its [[sequent calculus]] relies on the structure of order varieties (a family of [[cyclic order]]s that may be viewed as a [[combinatorial species|species of structure]]), and the correctness criterion for its [[proof net]]s is given in terms of [[partial permutation]]s. It also has a [[denotational semantics]] in which [[formula (logic)|formula]]s are interpreted by [[module (algebra)|module]]s over some specific [[Hopf algebra]]s.

==Noncommutativity in logic==

By extension, the term noncommutative logic is also used by a number of authors to refer to a family of [[substructural logics]] in which the [[structural rule|exchange rule]] is [[inadmissible inference rule|inadmissible]]. The remainder of this article is devoted to a presentation of this acceptance of the term.

The oldest noncommutative logic is the [[Lambek calculus]], which gave rise to the class of logics known as [[categorial grammar]]s. Since the publication of [[Jean-Yves Girard]]'s [[linear logic]] there have been several new noncommutative logics proposed, namely the [[cyclic linear logic]] of David Yetter, the [[pomset logic]] of Christian Retoré, and the noncommutative logics [[Noncommutative logic#BV and NEL|BV and NEL]].

Noncommutative logic is sometimes called ordered logic, since it is possible with most proposed noncommutative logics to impose a [[total order|total]] or [[partial order]] on the formulas in sequents. However this is not fully general since some noncommutative logics do not support such an order, such as Yetter's cyclic linear logic. Although most noncommutative logics do not allow weakening or contraction together with noncommutativity, this restriction is not necessary.

===The Lambek calculus===
{{main|categorial grammar}}

[[Joachim Lambek]] proposed the first non-commutative logic in his 1958 paper ''Mathematics of Sentence Structure'' to model the combinatory possibilities of the [[syntax]] of [[natural languages]].<ref>{{Cite journal| doi = 10.2307/2310058| issn = 0002-9890| volume = 65| issue = 3| pages = 154–170| last = Lambek| first = Joachim| title = The Mathematics of Sentence Structure| journal = [[The American Mathematical Monthly]]| date = 1958| jstor = 2310058|citeseerx=10.1.1.538.885}}</ref> In his subsequent 1961 paper ''On the calculus of syntactic types'', he extended the analysis to cover [[non-associativity]] as well. His calculus has since become one of the fundamental formalisms of [[computational linguistics]].

===Cyclic linear logic===

David N. Yetter proposed a weaker structural rule in place of the exchange rule of linear logic, yielding cyclic linear logic.<ref>{{Cite journal| doi = 10.2307/2274953| issn = 0022-4812| volume = 55| issue = 1| pages = 41–64| last = Yetter| first = David N.| title = Quantales and (Noncommutative) Linear Logic| journal = [[The Journal of Symbolic Logic]]| date = 1990| jstor = 2274953| hdl = 10338.dmlcz/140417| s2cid = 30626492}}</ref> Sequents of cyclic linear logic form a cycle, and so are invariant under rotation, where multipremise rules glue their cycles together at the formulas described in the rules. The calculus supports three structural modalities, a self-dual modality allowing exchange, but still linear, and the usual exponentials (? and !) of linear logic, allowing nonlinear structural rules to be used together with exchange.

===Pomset logic===

Pomset logic was proposed by Christian Retoré in a semantic formalism with two dual sequential operators existing together with the usual tensor product and par operators of linear logic, the first logic proposed to have both commutative and noncommutative operators.<ref>{{Cite book| publisher = Springer Berlin Heidelberg| isbn = 978-3-540-62688-6| pages = 300–318|editor1= Philippe de Groote |editor2=[[J. Roger Hindley]] | last = Retoré| first = Christian| title = Typed Lambda Calculi and Applications| volume = 1210| chapter = Pomset logic: A non-commutative extension of classical linear logic| series = Lecture Notes in Computer Science| date = 1997-04-02| doi=10.1007/3-540-62688-3_43|citeseerx=10.1.1.47.2354}}</ref> A sequent calculus for the logic was given, but it lacked a [[cut-elimination theorem]]; instead the sense of the calculus was established through a denotational semantics.

===BV and NEL===

[[Alessio Guglielmi]] proposed a variation of Retoré's calculus, BV, in which the two noncommutative operations are collapsed onto a single, self-dual, operator, and proposed a novel proof calculus, the [[calculus of structures]] to accommodate the calculus. The principal novelty of the calculus of structures was its pervasive use of [[deep inference]], which it was argued is necessary for calculi combining commutative and noncommutative operators; this explanation concurs with the difficulty of designing sequent systems for pomset logic that have cut-elimination.

Lutz Straßburger devised a related system, NEL, also in the calculus of structures in which linear logic with the mix rule appears as a subsystem.

==See also==
* [[Ordered type system]], a [[substructural type system]]
* [[Quantum logic]]

==References==
{{Reflist}}

==External links==
*[https://dx.doi.org/10.1016/S0168-0072(99)00014-7 Non-commutative logic I: the multiplicative fragment] by V. Michele Abrusci and Paul Ruet, [[Annals of Pure and Applied Logic]] 101(1), 2000.
*[https://www.lirmm.fr/~retore/ARTICLES/INTRO-LACL.pdf Logical aspects of computational linguistics] by Patrick Blackburn, Marc Dymetman, Alain Lecomte, Aarne Ranta, Christian Retoré and Eric Villemonte de la Clergerie.
*[http://alessio.guglielmi.name/res/cos/CNCLL/index.html Papers on Commutative/Non-commutative Linear Logic in the calculus of structures]: a research homepage from which the papers proposing BV and NEL are available.

{{DEFAULTSORT:Noncommutative Logic}}
[[Category:Substructural logic]]

Structural rule

2025-10-28T17:31:51Z

2A02:1812:110C:DC00:FD52:FD63:CF55:6615:

{{Short description|Rule of mathematical logic}}
{{for|the type of rule used in linguistics|phrase structure rule}}
In the [[formal logic|logical]] discipline of [[proof theory]], a '''structural rule''' is an [[inference rule]] of a [[sequent calculus]] that does not refer to any [[logical connective]] but instead operates on the [[sequent]]s directly.<ref name=":0">{{Cite journal |last=Gentzen |first=Gerhard |authorlink = Gerhard Gentzen|date=1935 |title=Untersuchungen über das logische Schließen. I, Mathematische Zeitschrift |url=http://link.springer.com/10.1007/BF01201353 |journal=[[Mathematische Zeitschrift]] |language=de |volume=39 |issue=1 |pages=176–210 |doi=10.1007/BF01201353 |issn=0025-5874|url-access=subscription }}</ref><ref>{{Cite book |last=Szabo |first=M. E. |title=Collected papers of Gerhard Gentzen |date=1969 |publisher=Elsevier |isbn=978-0-444-53419-4 |location=Place of publication not identified}}</ref> Structural rules often mimic the intended meta-theoretic properties of the logic. Logics that deny one or more of the structural rules are classified as [[substructural logic]]s.

==Common structural rules==
Three common structural rules are:<ref>{{Cite journal |last=Jacobs |first=Bart |date=1994 |title=Semantics of weakening and contraction |url=https://linkinghub.elsevier.com/retrieve/pii/0168007294900205 |journal=[[Annals of Pure and Applied Logic]] |language=en |volume=69 |issue=1 |pages=73–106 |doi=10.1016/0168-0072(94)90020-5|url-access=subscription }}</ref>

* '''{{vanchor|Weakening}}''', where the hypotheses or conclusion of a sequence may be extended with additional members. In symbolic form weakening rules can be written as <math>\frac{\Gamma \vdash \Sigma}{\Gamma, A \vdash \Sigma}</math> on the left of the [[Turnstile (symbol)|turnstile]], and <math>\frac{\Gamma \vdash \Sigma}{\Gamma \vdash \Sigma, A}</math> on the right. Known as [[monotonicity of entailment]] in classical logic.

* '''{{vanchor|Contraction}}''', where two equal (or unifiable) members on the same side of a sequent may be replaced by a single member (or common instance). Symbolically: <math>\frac{\Gamma, A, A \vdash \Sigma}{\Gamma, A \vdash \Sigma}</math> and <math>\frac{\Gamma \vdash A, A, \Sigma}{\Gamma \vdash A, \Sigma}</math>. Also known as '''factoring''' in [[automated theorem proving]] systems using [[Resolution (logic)|resolution]]. Known as '''idempotency of entailment''' in classical logic.
* '''Exchange''', where two members on the same side of a sequent may be swapped. Symbolically: <math>\frac{\Gamma_1, A, \Gamma_2, B, \Gamma_3 \vdash \Sigma}{\Gamma_1, B, \Gamma_2, A, \Gamma_3 \vdash \Sigma}</math> and <math>\frac{\Gamma \vdash \Sigma_1, A, \Sigma_2, B, \Sigma_3}{\Gamma \vdash \Sigma_1, B, \Sigma_2, A, \Sigma_3}</math>. (This is also known as the ''permutation rule''.)

A logic without any of the above structural rules would interpret the sides of a sequent as pure [[sequence]]s; with exchange, they can be considered to be [[multiset]]s; and with both contraction and exchange they can be considered to be [[set (mathematics)|set]]s.

These are not the only possible structural rules. A famous structural rule is known as '''[[cut rule|cut]]'''.<ref name=":0" /> Considerable effort is spent by proof theorists in showing that cut rules are superfluous in various logics. More precisely, what is shown is that cut is only (in a sense) a tool for abbreviating proofs, and does not add to the theorems that can be proved. The successful 'removal' of cut rules, known as ''[[Cut-elimination theorem|cut elimination]]'', is directly related to the philosophy of ''[[computation]] as normalization'' (see [[Curry–Howard correspondence]]); it often gives a good indication of the [[computational complexity theory|complexity]] of [[decision problem|deciding]] a given logic.

==See also==
*{{annotated link|Affine logic}}
*{{annotated link|Linear logic}}
*{{annotated link|Ordered logic (linear logic)}}
*{{annotated link|Relevance logic}}
*{{annotated link|Separation logic}}

==References==
{{Reflist}}

{{Non-classical logic}}

[[Category:Proof theory]]
[[Category:Rules of inference]]

Categorial grammar

2025-10-28T14:01:13Z

2A02:1812:110C:DC00:FD52:FD63:CF55:6615:

{{short description|Family of formalisms in natural language syntax}}
'''Categorial grammar''' is a family of formalisms in [[natural language]] [[syntax]] that share the central assumption that [[constituent (linguistics)|syntactic constituents]] combine as [[Function (mathematics)|function]]s and [[Argument of a function|arguments]]. Categorial grammar posits a close relationship between the syntax and [[compositionality|semantic composition]], since it typically treats syntactic categories as corresponding to semantic types. Categorial grammars were developed in the 1930s by [[Kazimierz Ajdukiewicz]] and in the 1950s by [[Yehoshua Bar-Hillel]] and [[Joachim Lambek]]. It saw a surge of interest in the 1970s following the work of [[Richard Montague]], whose [[Montague grammar]] assumed a similar view of syntax. It continues to be a major paradigm, particularly within [[formal semantics (natural language)|formal semantics]].

==Basics==
A categorial grammar consists of two parts: a lexicon, which assigns a set of types (also called categories) to each basic symbol, and some [[type inference]] rules, which determine how the type of a [[String (computer science)|string]] of symbols follows from the types of the constituent symbols. It has the advantage that the type inference rules can be fixed once and for all, so that the specification of a particular language grammar is entirely determined by the lexicon.

A categorial grammar shares some features with the [[simply typed lambda calculus]].
Whereas the [[lambda calculus]] has only one function type <math>A \rightarrow B</math>,
a categorial grammar typically has two function types, one type that is applied on the left,
and one on the right. For example, a simple categorial grammar might have two function types <math>B/A\,\!</math> and <math>A\backslash B</math>.
The first, <math>B/A\,\!</math>, is the type of a phrase that results in a phrase of type
<math>B\,\!</math> when followed (on the right) by a phrase of type <math>A\,\!</math>.
The second, <math>A\backslash B\,\!</math>, is the type of a phrase that results
in a phrase of type <math>B\,\!</math> when preceded (on the left) by a phrase of type
<math>A\,\!</math>.

The notation is based upon [[abstract algebra|algebra]]. A fraction when multiplied by (i.e. [[concatenated]] with) its denominator yields its numerator. As concatenation is not [[commutative]], it makes a difference whether the denominator occurs to the left or right. The concatenation must be on the same side as the denominator for it to cancel out.

The first and simplest kind of categorial grammar is called a basic categorial grammar, or sometimes an AB-grammar (after [[Ajdukiewicz]] and [[Yehoshua Bar-Hillel|Bar-Hillel]]).
Given a set of primitive types <math>\text{Prim}\,\!</math>, let
<math>\text{Tp}(\text{Prim})\,\!</math> be the set of types constructed from primitive types. In the basic case, this is the least set such that <math>\text{Prim}\subseteq \text{Tp}(\text{Prim})</math>
and if <math>X, Y\in \text{Tp}(\text{Prim})</math>
then <math>(X/Y), (Y\backslash X) \in \text{Tp}(\text{Prim})</math>.
Think of these as purely formal expressions freely generated from the primitive types; any semantics will be added later. Some authors assume a fixed infinite set of primitive types used by all grammars, but by making the primitive types part of the grammar, the whole construction is kept finite.

A basic categorial grammar is a tuple <math>(\Sigma, \text{Prim}, S, \triangleleft)</math>
where <math>\Sigma\,\!</math> is a finite set of symbols,
<math>\text{Prim}\,\!</math> is a finite set of primitive types, and <math>S \in \text{Tp}(\text{Prim})</math>.

The relation <math>\triangleleft</math> is the lexicon, which relates types to symbols <math>(\triangleleft) \subseteq \text{Tp}(\text{Prim}) \times \Sigma</math>.
Since the lexicon is finite, it can be specified by listing a set of pairs like <math>TYPE\triangleleft\text{symbol}</math>.

Such a grammar for English might have three basic types <math>(N,NP, \text{ and } S)\,\!</math>, assigning [[count noun]]s the type <math>N\,\!</math>, complete noun phrases the type
<math>NP\,\!</math>, and sentences the type <math>S\,\!</math>.
Then an [[adjective]] could have the type <math>N/N\,\!</math>, because if it is followed by a noun then the whole phrase is a noun.
Similarly, a [[determiner (linguistics)|determiner]] has the type <math>NP/N\,\!</math>,
because it forms a complete noun phrase when followed by a noun.
Intransitive [[verb]]s have the type <math>NP\backslash S</math>, and transitive verbs the type <math>(NP\backslash S)/NP</math>.
Then a string of words is a sentence if it has overall type <math>S\,\!</math>.

For example, take the string "the bad boy made that mess". Now "the" and "that" are determiners, "boy" and "mess" are nouns, "bad" is an adjective, and "made" is a transitive verb, so the lexicon is
{<math>NP/N\triangleleft\text{the}</math>,
<math>NP/N\triangleleft\text{that}</math>,
<math>N\triangleleft\text{boy}</math>,
<math>N\triangleleft\text{mess}</math>,
<math>N/N\triangleleft\text{bad}</math>,
<math>(NP\backslash S)/NP\triangleleft\text{made}</math>}.

and the sequence of types in the string is

<math>
{\text{the}\atop {NP/N,}}
{\text{bad}\atop {N/N,}}
{\text{boy}\atop {N,}}
{\text{made}\atop {(NP\backslash S)/NP,}}
{\text{that}\atop {NP/N,}}
{\text{mess}\atop {N}}
</math>

now find functions and appropriate arguments and reduce them according to the two [[inference rule]]s
<math> X\leftarrow X/Y,\; Y</math> and
<math> X\leftarrow Y,\; Y\backslash X</math>:

<math>.\qquad NP/N,\; N/N,\; N,\; (NP\backslash S)/NP,\; \underbrace{NP/N,\; N}</math> 
<math>.\qquad NP/N,\; N/N,\; N,\; \underbrace{(NP\backslash S)/NP, \quad NP}</math> 
<math>.\qquad NP/N,\; \underbrace{N/N,\; N}, \qquad (NP\backslash S)</math> 
<math>.\qquad \underbrace{NP/N,\; \quad N},\; \qquad (NP\backslash S)</math> 
<math>.\qquad \qquad\underbrace{NP,\; \qquad (NP\backslash S)}</math> 
<math>.\qquad \qquad\qquad\quad\;\;\; S</math>

The fact that the result is <math>S\,\!</math> means that the string is a sentence, while the sequence of reductions shows that it can be parsed as ((the (bad boy)) (made (that mess))).

Categorial grammars of this form (having only function application rules) are equivalent in generative capacity to [[context-free grammar]]s and are thus often considered inadequate for theories of natural language syntax. Unlike context-free grammars, categorial grammars are [[lexicalized]], meaning that only a small number of (mostly language-independent) rules are employed, and all other syntactic phenomena derive from the lexical entries of specific words.

Another appealing aspect of categorial grammars is that it is often easy to assign them a compositional semantics, by first assigning [[interpretation type]]s to all the basic categories, and then associating all the [[derived category|derived categories]] with appropriate [[Function (mathematics)|function]] types. The interpretation of any constituent is then simply the value of a function at an argument. With some modifications to handle [[intensionality]] and [[Quantification (linguistics)|quantification]], this approach can be used to cover a wide variety of semantic phenomena.

==Lambek calculus==

A Lambek grammar is an elaboration of this idea that has a
concatenation operator for types, and several other inference rules.
Mati Pentus has shown that these still have the generative capacity of
context-free grammars.

For the Lambek calculus, there is a type concatenation
operator <math>\star</math>, so
that <math>\text{Prim}\subseteq \text{Tp}(\text{Prim})</math>
and if <math>X, Y\in \text{Tp}(\text{Prim})</math>
then <math>(X/Y), (X\backslash Y), (X\star Y)\in \text{Tp}(\text{Prim})</math>.

The Lambek calculus consists of several deduction rules, which specify
how type inclusion assertions can be derived. In the following
rules, upper case roman letters stand for types, and upper case Greek
letters stand for finite [[sequence (mathematics)|sequence]]s of types. Juxtaposition of sequences indicates concatenation. A [[sequent]] of the form
<math> X \leftarrow \Gamma </math>
can be read: a string is of type {{mvar|X}} if it consists of the concatenation
of strings of each of the types in {{math|Γ}}. If a type is
interpreted as a set of strings, then the
← may be interpreted as &supe;,
that is, "includes as a subset".
A horizontal line means that the inclusion above the line
implies the one below the line.

The process is begun by the Axiom rule, which has no antecedents and
just says that any type includes itself.

:<math>
\text{(Axiom)}\quad
{{}\over X \leftarrow X}
</math>

The Cut rule says that inclusions can be composed.

:<math>
\text{(Cut)} \quad
{Z \leftarrow \Delta X \Delta' \qquad X \leftarrow \Gamma
\over
Z \leftarrow \Delta \Gamma \Delta'}
</math>

The other rules come in pairs, one pair for each type construction
operator, each pair consisting of one rule for the operator in the
target, one in the source, of the arrow.
The name of a rule consists of the operator and an arrow, with the
operator on the side of the arrow on which it occurs in the conclusion.

:{| class="wikitable"
|-
!Target
!Source
|-
|<math>
(\backslash \leftarrow) \quad
{Y\leftarrow X \Gamma
\over
X\backslash Y\leftarrow\Gamma}
</math>
|<math>
(\leftarrow \backslash) \quad
{Z \leftarrow \Delta Y \Delta' \qquad X\leftarrow\Gamma
\over
Z \leftarrow \Delta \Gamma(X\backslash Y) \Delta'}
</math>
|-
|<math>
(/\leftarrow) \quad
{Y\leftarrow \Gamma X
\over
Y/X\leftarrow\Gamma}
</math>
|<math>
(\leftarrow/) \quad
{Z\leftarrow \Delta Y \Delta' \qquad X\leftarrow\Gamma
\over
Z\leftarrow \Delta (Y/X)\Gamma \Delta'}
</math>
|-
|<math>
(\star\leftarrow) \quad {X\leftarrow \Gamma \qquad Y \leftarrow \Gamma'
\over
X \star Y \leftarrow \Gamma\Gamma'}
</math>
|<math>
(\leftarrow\star) \quad {Z\leftarrow \Delta X Y \Delta'
\over
Z\leftarrow \Delta (X \star Y) \Delta'}
</math>
|}

For an example, here is a derivation of "type raising", which says that
<math>(B/A)\backslash B \leftarrow A</math>. The names of rules and the substitutions used are to the right.

:<math>
\dfrac {\dfrac{}{B \leftarrow B} \qquad \dfrac{}{A \leftarrow A} }
{\dfrac {B \leftarrow (B/A), \;\; A}
{(B/A)\backslash B \leftarrow A} }
\qquad
\begin{matrix}
\mbox{(Axioms)}\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad{ }\\
{(\leftarrow/)\,\,[Z=Y=B,X=A,\Gamma=(A),\Delta=\Delta'=()]}\\
{(\backslash\leftarrow)\,\,[Y=B,X=(B/A),\Gamma=(A)]}\qquad\qquad\qquad{ }\\
\end{matrix}
</math>

===Relation to context-free grammars===

Recall that a [[context-free grammar]] is a 4-tuple <math>G = (V,\, \Sigma,\, ::=,\, S)</math> where

# <math>V\, </math> is a finite set of ''non-terminals'' or ''variables''.
# <math>\Sigma\,</math> is a finite set of ''terminal symbols''.
# <math>::=\,</math> is a finite set of [[Production rule (formal languages)|production rules]], that is, a finite relation <math>(::=)\subseteq V \times (V \cup \Sigma)^*</math>.
# <math>S\,</math> is the start variable.

From the point of view of categorial grammars, a context-free grammar can be seen as a calculus with a set of special purpose axioms for
each language, but with no type construction operators and no inference rules except Cut.

Specifically, given a context-free grammar as above, define a categorial grammar
<math>(\text{Prim},\, \Sigma,\, \triangleleft,\, S)</math>
where <math>\text{Prim}=V\cup\Sigma</math>,
and <math>\text{Tp}(\text{Prim})=\text{Prim}\,\!</math>.
Let there be an axiom
<math>{x \leftarrow x}</math> for every symbol
<math>x \in V\cup\Sigma</math>,
an axiom <math>{X \leftarrow \Gamma}</math>
for every production rule <math>X ::= \Gamma\,\!</math>,
a lexicon entry <math>{s \triangleleft s}</math> for every terminal symbol
<math>s \in \Sigma</math>,
and Cut for the only rule.
This categorial grammar generates the same language as the given context-free grammar.

Of course, this is not a basic categorial grammar, since it has special axioms that depend upon the language; i.e. it is not lexicalized.
Also, it makes no use at all of non-primitive types.

To show that any context-free language can be generated by a basic categorial grammar, recall that
any context-free language can be generated by a context-free grammar in [[Greibach normal form]].

The grammar is in Greibach normal form if every production rule is of the form
<math> A ::= s A_0 \ldots A_{N-1}</math>,
where capital letters are variables, <math>s \in \Sigma</math>,
and <math>N\ge 0</math>,
that is, the right side of the production is a single terminal symbol
followed by zero or more (non-terminal) variables.

Now given a context-free grammar in Greibach normal form,
define a basic categorial grammar with a primitive type
for each non-terminal variable
<math>\text{Prim}=V\,\!</math>,
and with an entry in the lexicon
<math> A/A_{N-1}/ \ldots /A_0 \triangleleft s </math>,
for each production rule
<math> A ::= s A_0 \ldots A_{N-1}</math>.
It is fairly easy to see that this basic categorial grammar
generates the same language as the original context-free grammar.
Note that the lexicon of this grammar will generally
assign multiple types to each symbol.

The same construction works for Lambek grammars, since they are an extension of basic categorial grammars. It is necessary to verify that the extra inference rules do not change the generated language. This can be done and shows that every context-free language is generated by some Lambek grammar.

To show the converse, that every language generated by a Lambek grammar is context-free, is much more difficult.
It was an open problem for nearly thirty years, from the early 1960s until about 1991 when it was proven by Pentus.

The basic idea is, given a Lambek grammar,
<math>(\text{Prim},\, \Sigma,\, \triangleleft,\, S)</math>
construct a context-free grammar
<math>(V,\, \Sigma,\, ::=,\, S)</math>
with the same set of terminal symbols, the same start symbol, with variables some (not all) types
<math>V\subseteq \text{Tp}(\text{Prim})\,\!</math>,
and with a production rule
<math>T::=\text{s}\,\!</math>
for each entry
<math>T\triangleleft\text{s}</math>
in the lexicon, and production rules <math>T::=\Gamma\,\!</math> for certain sequents <math>T\leftarrow\Gamma</math> that are derivable in the Lambek calculus.

Of course, there are infinitely many types and infinitely many derivable sequents, so in
order to make a finite grammar it is necessary put a bound on the size of the types and sequents
that are needed. The heart of Pentus's proof is to show that there is such a finite bound.

===Notation===
The notation in this field is not standardized. The notations used in
[[formal language theory]], [[formal logic|logic]], [[category theory]], and [[linguistics]], conflict
with each other. In logic, arrows point to the more general from the more particular,
that is, to the conclusion from the hypotheses. In this article,
this convention is followed, i.e. the target of the arrow is the more general (inclusive) type.

In logic, arrows usually point left to right. In this article this convention is
reversed for consistency with the notation of context-free grammars, where the
single non-terminal symbol is always on the left. We use the symbol <math>::=</math>
in a production rule as in [[Backus–Naur form]]. Some authors use an arrow, which
unfortunately may point in either direction, depending on whether the grammar is
thought of as generating or recognizing the language.

Some authors on categorial grammars write <math>B\backslash A</math> instead of
<math>A\backslash B</math>. The convention used here follows Lambek and algebra.

==Historical notes==
The basic ideas of categorial grammar date from work by [[Kazimierz Ajdukiewicz]] (in 1935) and other scholars from the Polish tradition of [[mathematical logic]] including [[Stanisław Leśniewski]], [[Emil Leon Post|Emil Post]] and [[Alfred Tarski]]. Ajdukiewicz's formal approach to syntax was influenced by [[Edmund Husserl|Edmund Husserl's]] [[Logical grammar|pure logical grammar]], which was formalized by [[Rudolf Carnap|Rudolph Carnap]]. It represents a development in the historical idea of universal logical grammar as an underlying structure of all languages. A core concept of the approach is the substitutability of syntactic categories—hence the name categorial grammar. The membership of an element (e.g., word or phrase) in a syntactic category (word class, phrase type) is established by the [[commutation test]], and the [[formal grammar]] is constructed through series of such tests.<ref>{{cite journal |last1=Wybraniec-Skardowska |first1=Urszula |last2=Rogalski |first2=Andrzej K. |date=1998 |title=On universal grammar and its formalization |url=https://www.pdcnet.org/collection/fshow?id=wcp20-paideia_1998_0008_0153_0172&pdfname=wcp20-paideia_1998_0008_0153_0172.pdf&file_type=pdf |journal=The Paideia Archive: Twentieth World Congress of Philosophy |volume=8 |issue= |pages=153–172 |doi= 10.5840/wcp20-paideia19988195|isbn=978-1-63435-051-8 |access-date=2023-09-05|url-access=subscription }}</ref>

The term categorial grammar was coined by [[Yehoshua Bar-Hillel]] (in 1953). In 1958, [[Joachim Lambek]] introduced a [[Lambek Calculus|syntactic calculus]] that formalized the function [[type constructors]] along with various rules for the combination of functions. This calculus is a forerunner of [[linear logic]] in that it is a [[substructural logic]].

[[Montague grammar]] is based on the same principles as categorial grammar.<ref>{{Cite book |last1=Partee |first1=Barbara Hall |title=[Richard] Montague grammar: Ed. by Barbara H[all] Partee |last2=Montague |first2=Richard |date=1976 |publisher=Acad. Pr |isbn=978-0-12-545850-4 |location=New York [usw.]}}</ref> [[Richard Montague|Montague's]] work helped to bolster interest in categorial grammar by associating it with his highly successful formal treatment of natural language [[semantics]]. Later work in categorial grammar has focused on the improvement of syntactic coverage. One formalism that has received considerable attention in recent years is [[Mark Steedman|Steedman]] and [[Anna Szabolcsi|Szabolcsi]]'s [[combinatory categorial grammar]], which builds on [[combinatory logic]] invented by [[Moses Schönfinkel]] and [[Haskell Curry]].

There are a number of related formalisms of this kind in linguistics, such as [[type logical grammar]] and [[abstract categorial grammar]].<ref>{{Cite book |last=Morrill |first=Glyn |title=Type logical grammar: categorial logic of signs |date=1994 |publisher=Kluwer |isbn=978-0-7923-3095-0 |location=Dordrecht}}</ref><ref>{{Cite conference|last= De Groote|first= Philippe |title= Towards abstract categorial grammars |date= 2001 |book-title= Proceedings of the 39th Annual Meeting of the Association for Computational Linguistics|pp= 252–259|url= https://aclanthology.org/P01-1033.pdf}}</ref>

==Some definitions==
;Derivation: A derivation is a [[binary tree]] that encodes a proof.
;[[Parse tree]]: A parse tree displays a derivation, showing the syntactic structure of a sentence.
;Functor and argument: In a right (left) function application, the node of the type A\B (B/A) is called the functor, and the node of the type A is called an argument.
;Functor–argument structure{{clarify| where's the definition?|date=July 2015}}

==Refinements of categorical grammar==
A variety of changes to categorial grammar have been proposed to improve syntactic coverage. Some of the most common are listed below.

===Features and subcategories===
Most systems of categorial grammar subdivide categories. The most common way to do this is by tagging them with [[grammatical feature|features]], such as [[Grammatical person|person]], [[Grammatical gender|gender]], [[Grammatical number|number]], and [[Grammatical tense|tense]]. Sometimes only atomic categories are tagged in this way. In Montague grammar, it is traditional to subdivide function categories using a multiple slash convention, so ''A/B'' and ''A//B'' would be two distinct categories of left-applying functions, that took the same arguments but could be distinguished between by other functions taking them as arguments.

===Function composition===
Rules of function composition are included in many categorial grammars. An example of such a rule would be one that allowed the concatenation of a constituent of type ''A/B'' with one of type ''B/C'' to produce a new constituent of type ''A/C''. The semantics of such a rule would simply involve the composition of the functions involved. Function composition is important in categorial accounts of [[logical conjunction|conjunction]] and extraction, especially as they relate to phenomena like [[right node raising]]. The introduction of function composition into a categorial grammar leads to many kinds of derivational ambiguity that are vacuous in the sense that they do not correspond to [[semantic ambiguity|semantic ambiguities]].

===Conjunction===
Many categorial grammars include a typical conjunction rule, of the general form ''X CONJ X → X'', where ''X'' is a category. Conjunction can generally be applied to nonstandard constituents resulting from type raising or function composition.

===Discontinuity===
The grammar is extended to handle linguistic phenomena such as discontinuous idioms, gapping and extraction.<ref>{{Cite book |last=Huck |first=Geoffrey J. |title=Discontinuity and Word Order in Categorial Grammar |publisher=Indiana University Linguistics Club |year=1985}}</ref>

==See also==
*[[Combinatory categorial grammar]]
*[[Link grammar]]
*[[Noncommutative logic]]
*[[Pregroup Grammar]]
*[[Scope (formal semantics)|Scope]]
*[[Type shifter]]

==References==
{{Reflist}}
*{{citation |last1=Curry|first1=Haskell B.|author1-link=Haskell Curry |first2=Richard |last2= Feys|year=1958 | title= Combinatory Logic |volume= 1 |publisher=North-Holland}}
*{{citation |last1=Jacobson|first1= Pauline|author1-link=Pauline Jacobson |title=Towards a variable-free semantics. |journal=[[Linguistics and Philosophy]]|volume=22|issue= 2|year=1999 |pages=117–184|doi= 10.1023/A:1005464228727|s2cid= 60578091}}
*{{citation |last1=Lambek |first1=Joachim|author1-link=Joachim Lambek|year=1958 |title=The mathematics of sentence structure |journal=[[American Mathematical Monthly|Amer. Math. Monthly]]|volume= 65 |issue=3|pages=154–170|citeseerx=10.1.1.538.885|doi=10.1080/00029890.1958.11989160}}
*{{citation |last1=Pentus |first1= Mati |year=1997 |title=Lambek Calculus and Formal Grammars| publisher= Amer. Math. Soc. Transl.|url=http://158.250.33.126/~pentus/ftp/papers/ams.pdf}}
*{{citation |last1=Steedman|first1=Mark |author1-link=Mark Steedman|year=1987 |title=Combinatory grammars and parasitic gaps |journal=[[Natural Language and Linguistic Theory]] |volume=5|issue=3 |pages=403–439|doi=10.1007/bf00134555|s2cid=170899264 }}
*{{citation |last1=Steedman|first1= Mark |author1-link=Mark Steedman|year=1996 |title=Surface Structure and Interpretation|publisher=[[The MIT Press]]}}
*{{citation |last1=Steedman|first1=Mark |author1-link=Mark Steedman |year=2000 | title=The Syntactic Process |publisher=[[The MIT Press]]}}
*{{cite book |last1=Szabolcsi|first1=Anna|year=1989|chapter=Bound variables in syntax (are there any?)|title=Semantics and Contextual Expression| editor1-last=Bartsch|editor2-last=van Benthem|editor3= van Emde Boas|publisher= Foris |pages=294–318|chapter-url=https://philpapers.org/archive/SZABVI.pdf}}
*{{cite book |last1=Szabolcsi |first1=Anna |year=1992 |chapter=Combinatory grammar and projection from the lexicon|title=Lexical Matters|journal=[[CSLI Lecture Notes]]|volume=24|editor1=Sag|editor2= Szabolcsi |location=Stanford |publisher=CSLI Publications |pages= 241–269|chapter-url=http://www.u.tsukuba.ac.jp/~kubota.yusuke.fn/lsa/szabolcsi92.pdf}}
*{{citation |last1=Szabolcsi |first1=Anna |title=Resource-Sensitivity, Binding and Anaphora |chapter=Binding on the Fly: Cross-Sentential Anaphora in Variable-Free Semantics |year=2003 |volume=80 |editor1= Kruijff |editor2=Oehrle |publisher=Kluwer |pages=215–229|doi=10.1007/978-94-010-0037-6_8|series=Studies in Linguistics and Philosophy |isbn=978-1-4020-1692-9 |citeseerx=10.1.1.205.3142 }}
*{{citation |last1=Morril |first1=Glyn |year=1995 |title=Discontinuity in categorial grammar |journal=Linguistics and Philosophy |volume=18 |issue=2 |pages=175–219|doi=10.1007/bf00985216|s2cid=62533943 }}

==Further reading==
* Michael Moortgat, ''Categorial Type Logics'', Chapter 2 in J. van Benthem and [[Alice ter Meulen|A. ter Meulen]] (eds.) ''Handbook of Logic and Language''. Elsevier, 1997, {{ISBN|0-262-22053-9}}
* Wojciech Buszkowski, ''Mathematical linguistics and proof theory'', Chapter 12 in J. van Benthem and [[Alice ter Meulen|A. ter Meulen]] (eds.) ''Handbook of Logic and Language''. Elsevier, 1997, {{ISBN|0-262-22053-9}}
* {{cite book|author=Gerhard Jäger|title=Anaphora and Type Logical Grammar|year=2005|publisher=Springer|isbn=978-1-4020-3904-1}}
* {{cite book|author=Glyn Morrill|title=Categorial Grammar: Logical Syntax, Semantics, and Processing|year=2010|publisher=Oxford University Press|isbn=978-0-19-958986-9}}
* {{cite book|author1=Richard Moot|author2=Christian Retoré|title=The Logic of Categorial Grammars: A Deductive Account of Natural Language Syntax and Semantics|year=2012|publisher=Springer Verlag|isbn=978-3-642-31554-1}}

==External links==
* [https://encyclopediaofmath.org/wiki/Grammar,_categorial Grammar, categorial] at Springer [[Encyclopaedia of Mathematics]]
* [https://plato.stanford.edu/entries/typelogical-grammar/ Typelogical Grammar] at [[Stanford Encyclopedia of Philosophy]]

{{Formal semantics}}

[[Category:Grammar frameworks]]
[[Category:Formal languages]]
[[Category:Computational linguistics]]
[[Category:Type theory]]
[[Category:Semantics]]
[[Category:Mathematical linguistics]]

Proof net

2025-10-27T18:59:02Z

2A02:1812:110C:DC00:FD52:FD63:CF55:6615:

In [[proof theory]], '''proof nets''' are a geometrical method of representing proofs that
eliminates two forms of ''bureaucracy'' that differentiate proofs: (A) irrelevant syntactical features of regular [[proof calculi]], and (B) the order of rules applied in a derivation. In this way, the formal properties of proof identity correspond more closely to the intuitively desirable properties. This distinguishes proof nets from regular proof calculi such as the [[natural deduction]] calculus and the [[sequent calculus]], where these phenomena are present. Proof nets were introduced by [[Jean-Yves Girard]].

As an illustration, these two [[linear logic]] proofs are identical:

{| style="margin:0.5em auto"
|-
| style="text-align: center; padding-right: 40px" |
{| border="0"
|-
| {{math|{{tee}} <VAR>A</VAR>, <VAR>B</VAR>, <VAR>C</VAR>, <VAR>D</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} <VAR>A</VAR> ⅋ <VAR>B</VAR>, <VAR>C</VAR>, <VAR>D</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} <VAR>A</VAR> ⅋ <VAR>B</VAR>, <VAR>C</VAR> ⅋ <VAR>D</VAR>}}
|}
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} <VAR>A</VAR>, <VAR>B</VAR>, <VAR>C</VAR>, <VAR>D</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} <VAR>A</VAR>, <VAR>B</VAR>, <VAR>C</VAR> ⅋ <VAR>D</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} <VAR>A</VAR> ⅋ <VAR>B</VAR>, <VAR>C</VAR> ⅋ <VAR>D</VAR>}}
|}
|}

And their corresponding nets will be the same.

== Correctness criteria ==
Several correctness criteria are known to check if a sequential proof structure (i.e. something that seems to be a proof net) is actually a concrete proof structure (i.e. something that encodes a valid derivation in linear logic). The first such criterion is the [[long-trip criterion]],<ref>Girard, Jean-Yves. ''[http://girard.perso.math.cnrs.fr/linear.pdf Linear logic]'', [[Theoretical Computer Science (journal)|Theoretical Computer Science]], Vol 50, no 1, pp. 1–102, 1987</ref> which was described by [[Jean-Yves Girard]].

==See also==
* [[Linear logic]]
* [[Ludics]]
* [[Geometry of interaction]]
* [[Coherent space]]
* [[Deep inference]]
* [[Interaction nets]]

==References==
<references />

==Sources ==
* ''[http://www.paultaylor.eu/stable/Proofs+Types.html Proofs and Types]''. Girard J-Y, Lafont Y, and Taylor P. Cambridge Press, 1989.
* [[Roberto Di Cosmo]] and Vincent Danos, [http://www.dicosmo.org/CourseNotes/LinLog/ The Linear Logic Primer]
* Sean A. Fulop, [https://arxiv.org/abs/1203.4912 A survey of proof nets and matrices for substructural logics]

[[Category:Proof theory]]

{{logic-stub}}