LK vs LJ: An origin story for linear logic

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 should be split into two connectives . 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.

   

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, -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 have exactly one formula on their right-hand side.

1. No structural rules are permitted on the right.
2. The two multiplicative rules, 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 L rule.

   

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 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 rule and a trivial implication, as illustrated by the following two inferences.

   

Thus, the restriction on 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 and stipulating that a formula of the form 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 and where 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 rule applied to the formula moves to the left-hand side, it is natural to encode that implication as , where is the linear implication. Such an encoding ensures that is affixed to 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

   

in which the multiset union is a single formula. The natural right-introduction rule for 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 and contain formulas marked for weakening and contraction. Thus, must be empty and, as a result, must be the single formula on the right of the concluding sequent. This explains the second restriction above, which concerns the structure of 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 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).