Skip to content

The Proof Theory Blog

PA ⊢ ∀x ∃y A(x,y) ⇒ ∃t . T ⊢ ∀x A(x,t(x))

Menu
  • Home
  • About
  • Contribute
  • Resources
Menu

LK vs LJ: An origin story for linear logic

Posted on July 6, 2022July 6, 2022 by Dale Miller

In his 1987 TCS paper [2], Girard credits semantic considerations related to coherent models as the origin of the key observation behind linear logic: the intuitionistic implication B\supset C should be split into two connectives \mathop{!} B\multimap C. To the extent that it makes sense to propose an alternative origin story for linear logic, it is interesting to note that Gentzen’s design of LJ as a restriction on LK provides another way to motivate this key observation.

A small adjustment to Gentzen’s formulation

To tell this origin story, we first make a small change to the logical connectives used in LK and LJ. In his 1935 paper [1], Gentzen treats negation as a logical connective by providing the following left and right introduction rules for negation.

    \[\infer{{\Gamma}\vdash{B,\Delta}}{{\neg B,\Gamma}\vdash{\Delta}}\qquad\infer{{\Gamma,B}\vdash{\Delta}}{{\Gamma}\vdash{\neg B, \Delta}}\]


Gentzen’s intuitionistic proof system LJ is defined as a restriction on LK in which all sequents have at most one formula on the right. With that restriction, \neg-left introduction can be used whenever the concluding sequent has an empty right-hand side. Instances of weakening on the right can also appear in Gentzen’s version of LJ proofs.

The small change we wish to make is the replacement of the logical connective for negation with “implies false”, where false is the additive false (i.e., its left-introduction rules allows for ex falso quodlibet). With this modification, the LJ proof system can be seen as the restriction of LK proofs in which sequents have exactly one formula on the right. Moreover, by removing negation as a connective, we have removed weakening on the right from LJ: it is absorbed into the left-introduction rule for false.

The following two restrictions guarantee that all sequents in an LK proof of the endsequent \ \vdash{B} have exactly one formula on their right-hand side.

  1. No structural rules are permitted on the right.
  2. The two multiplicative rules, \supset L and cut, are restricted so that the formula on the right-hand side of the conclusion must also be the formula on the right-hand side of the rightmost premise.

To illustrate this second restriction, recall the form of the \supsetL rule.

    \[\infer{{\Gamma_1}\vdash{\Delta_1,B}\qquad{C,\Gamma_2}\vdash{\Delta_2}}{B\supset C,\Gamma_1,\Gamma_2\vdash \Delta_1,\Delta_2}\]


Thus, in general, if the right-hand side of the conclusion contains one formula, that formula can move to the right-hand side of either the left or right premise. However, the restriction defining LJ forces that formula to move only to the right premise and not to the left. Thus, the \supset L rule in LJ proofs does two things: it introduces a connective and moves a side formula to a particular place. In this sense, implication within intuitionistic logic is different from all other logical connectives, which are only involved in introducing a connective (in either an additive or multiplicative fashion).

Recall that the cut rule can be emulated using the \supset L rule and a trivial implication, as illustrated by the following two inferences.

    \[\infer{{\Gamma_1}\vdash{\Delta_1,B}\qquad{B,\Gamma_2}\vdash{\Delta_2}}{{\Gamma_1,\Gamma_2}\vdash{\Delta_1, \Delta_2}}cut \qquad\infer{{\Gamma_1}\vdash{\Delta_1,B}\qquad {B,\Gamma_2}\vdash{\Delta_2}}{{\Gamma_1,\Gamma_2,B\supset B}\vdash{\Delta_1, \Delta_2}}\supset L,\]

Thus, the restriction on \supset L can explain the similar restriction on cut.

The single-conclusion restriction and the ! operator

In summary, the single-conclusion restriction on LJ proofs implies that

  1. the structural rules are available on the left-hand side of sequents but not on the right-hand side, and
  2. the implication has more internal structure than is apparent from its multiplicative inference rule.

These two facts motivate the key observation about linear logic in the following fashion. Since some occurrences of formulas in an LJ proof can be contracted while some cannot suggests marking formulas that can be weakened and contracted. This marking can be done using the operator \mathop{!} and stipulating that a formula of the form \mathop{!} B on the left-hand side can have weakening and contraction applied to them. Thus, sequents in LJ can be encoded using sequents of the form {\mathop{!} B_1,\ldots,\mathop{!} B_n}\vdash{B_0} and where B_0 is not marked for contraction and weakening. (In linear logic, the mark on the right-hand side is ?, the dual of !.)

The ! operator can also be used to explain the behavior of the intuitionistic implication. Since the \supset R rule applied to the formula B\supset C moves B to the left-hand side, it is natural to encode that implication as \mathop{!} B\multimap C, where \multimap is the linear implication. Such an encoding ensures that \mathop{!} is affixed to B as a new member of the left-hand side (reading proofs from conclusion to premises). This decomposition of the intuitionistic implication also explains the second restriction listed above. In particular, consider the following inference rule

    \[\infer[\multimapl]{{\Gamma_1}\vdash{\Delta_1,\mathop{!} B}\qquad {C,\Gamma_2}\vdash{\Delta_2}}{{\mathop{!} B\multimap C,\Gamma_1,\Gamma_2}\vdash {\Delta_1, \Delta_2}}\]


in which the multiset union \Delta_1,\Delta_2 is a single formula. The natural right-introduction rule for \mathop{!} is the promotion rule (in modal logic, this is also called the necessitation rule). This rule only applies to the left premise above if both \Gamma_1 and \Delta_1 contain formulas marked for weakening and contraction. Thus, \Delta_1 must be empty and, as a result, \Delta_2 must be the single formula on the right of the concluding sequent. This explains the second restriction above, which concerns the structure of \supset L in LJ.

Thus, Gentzen’s LK and LJ proof systems, with their use of the structural rules and the single-conclusion restriction for intuitionistic logic, can be seen as a clear motivation for splitting the intuitionistic implication into \mathop{!} and the linear implication. The rest of the story behind encoding full intuitionistic logic requires additional and careful treatment.

References

[1] Gentzen, Gerhard, 1934/35, “Untersuchungen über das logische Schließen I,II”, Mathematische Zeitschrift, 39: 176–210, 405–431. English translation, “Investigations into Logical Deduction”, in Gentzen 1969: 68–131 (doi).

[2] Girard, J.-Y., 1987, “Linear logic”, Theoretical Computer Science, 50: 1–102 (doi).

2 thoughts on “LK vs LJ: An origin story for linear logic”

  1. Anupam Das says:
    July 20, 2022 at 5:06 pm

    Hi Dale, thanks for the post! It is a nice viewpoint that the calculus LJ seems to suggest an exponential modality in order to control structural behaviour (on the right). However, it is not immediately clear to me that it induces the corresponding rules/axioms for ! in a canonical manner. Could one obtain a similar embedding of LJ into, say, Elementary Linear Logic (or some variant), where one/both of the axioms T : !A \multimap A (‘dereliction’) and 4: !A \multimap !!A (‘digging’) are dropped? (I’m sure this is known, but not yet to me).

    Reply
  2. Dale Miller says:
    July 23, 2022 at 9:28 am

    Dear Anupam, As you point out, there is nothing canonical about the possible treatments of the exponential modality in the sequent calculus. Besides the various treatments for them in Light Linear Logic, Soft Linear Logic, and Bounded Linear Logic, there is also the subexponentials approach. (References to these terms can be found in the Linear Logic article article in the SEP). In the story I gave, where !A marks A as a formula that can be contracted or weakened, it was assumed that such markings are not lost during promotion and that at any moment, the top-level connective of A could be introduced (hence, dereliction is always available). These choices align well with the LK/LJ comparison, but there are many other choices if one is not trying to capture the LJ restriction on LK.

    Reply

Leave a Reply Cancel reply

Your email address will not be published. Required fields are marked *

Meta

  • Register
  • Log in
  • Entries RSS
  • Privacy Policy

Search

© 2023 The Proof Theory Blog | Powered by Minimalist Blog WordPress Theme
The Proof Theory Blog uses cookies, but you can opt-out if you wish. For further information see our privacy policy. Cookie settingsAccept
Privacy & Cookies Policy

Privacy Overview

This website uses cookies to improve your experience while you navigate through the website. Out of these cookies, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities of the website. We also use third-party cookies that help us analyze and understand how you use this website. These cookies will be stored in your browser only with your consent. You also have the option to opt-out of these cookies. But opting out of some of these cookies may have an effect on your browsing experience.
Necessary
Always Enabled
Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.
Non-necessary
Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.
SAVE & ACCEPT