Varieties of linear calculi

Sara Negri (negri@helsinki.fi)

Department of Philosophy University of Helsinki

Abstract. A uniform calculus for linear logic is presented. The calculus has the form of a natural deduction system in sequent calculus style with general introduction and elimination rules. General elimination rules are motivated through an inversion principle, the dual form of which gives the general introduction rules. By restricting all the rules to their single-succedent versions, a uniform calculus for intuitionistic linear logic is obtained. The calculus encompasses both natural deduction and sequent calculus that are obtained as special instances from the uniform calculus. Other instances give all the invertibilities and partial invertibilities for the sequent calculus rules of linear logic. The calculus is normalizing and satisfies the subformula property for normal derivations.

1. Introduction

There is no general agreement on what features distinguish sequent calculus and natural deduction from each other. As soon as tentative characterizing properties are singled out, exceptions are found:

1. Sequent calculus has the structural rules of weakening, contraction, and cut, whereas natural deduction has no structural rules.

This first difference disappears in the family of cut- and contractionfree calculi G3 originated along the line Kleene-Dragalin-Troelstra and in other proof-search oriented calculi, like the G4 calculi, introduced by Hudelmaier and Dyckhoff and the calculi recently introduced by Miglioli and his collaborators for various intermediate logics (as in Avellone, Ferrari, and Miglioli 1999).

Besides these calculi, there exist sequent calculi in which the effect of the structural rules is achieved as in natural deduction, namely by vacuous and multiple discharge in the rules corresponding to elimination rules and to implication introduction (cf. Negri and von Plato 2001a).

In natural deduction, the absence, or better, implicit treatment of structural rules works to perfection only when treating contextindependent connectives. The simultaneous presence of context-sharing and context-independent connectives in linear logic breaks down the modularity needed in systems with implicit weakening and contraction; Consequently, systems of natural deduction for linear logic are often formulated with explicit structural rules.

\begin{matrix}c \\ ◯ \end{matrix} 2002 Kluwer Academic Publishers. Printed in the Netherlands.

2. In sequent calculus derivations are trees labelled by sequents, in natural deduction derivations are trees labelled by formulas.

3. In sequent calculus rules are local, in natural deduction they are nonlocal.

These two latter distinctions are based only on the notation chosen, as one may as well write natural deduction in sequent calculus style, with all active assumptions listed at each step of inference. Thus the rules of natural deduction can be made local. On the other hand, there are sequent calculi with nonlocal rules.

4. Rules of sequent calculus can have any number of formulas in the succedent, whereas rules of natural deduction have a single conclusion.

Although this is almost invariably the case, multiple-conclusion systems of natural deduction have been proposed (e.g., in Ungar 1992). Also, in the case of linear logic, proof-nets can be regarded as a multipleconclusion natural deduction system.

5. The basic structural requirement for sequent calculus is cut-elimination, and normalization for natural deduction.

The two features cannot be put in a 1-1 correspondence, in the sense that translating cut-free derivations into natural deduction can produce non-normalities, and translating normal derivations into sequent calculus can produce cuts.

In recent years sequent calculus has been brought closer to natural deduction by the elimination of redundancies which are absent in natural deduction, and sequent calculi have been formulated where normality of sequent derivations corresponds to normality for λ-terms (Herbelin 1994, Mints 1996, Dyckhoff and Pinto 1999).

Points 1–5 attempt to give characteristics that distinguish the two main varieties of logical calculi from each other. There are exceptions to each of the points, and these exceptions should give an indication of the work that has been done to bridge the gap between the two varieties. It is also clear that the borderline between the two varieties of logical calculi is even more vague for linear logic. In contrast to the well established system of natural deduction for intuitionistic logic, there is no unique answer to what a natural deduction system for linear logic should be.

The two approaches to proof theory have also been related in a more direct manner in Negri and von Plato (2001), through a uniform calculus, the rules of which contain as special instances the rules of sequent calculus and natural deduction.

The rules of the uniform calculus are found through the constructive meaning explanation of the logical connectives: First introduction rules are justified in proof-theoretical terms through the BHK-interpretation of the logical constants that gives the sufficient grounds for deriving a formula. General elimination rules can then be obtained from the introduction rules through an inversion principle stating that whatever follows from the sufficient grounds for deriving a formula must follow from that formula (cf. Section 2). Finally, general introduction rules are determined by a dual inversion principle stating that whatever follows from a formula must follow from the sufficient grounds for deriving the formula.

With the standard elimination rules there is no obvious correspondence between normal derivations in natural deduction and cut-free derivations in sequent calculus, since the translation of normal derivations produces sequent derivations with cuts and the translation of cut-free derivations produces non-normalities. With general elimination rules, instead, no cuts are introduced in the translation from normal natural deduction to sequent calculus, and no non-normalities arise in a translation of cut-free derivations.

We shall here extend to linear logic the application of the inversion principles in the design of a calculus with general rules. The calculus thus obtained will be flexible enough to give a variety of calculi as special cases, and at the same time structured enough so as to enjoy normalization and the subformula property for normal derivations.

General elimination rules for the connectives and for the modality ! of intuitionistic linear logic are used in Negri (2002) for obtaining a normalizing system of natural deduction, with no explicit structural rules and with a full subformula property.

The rules of the uniform calculus for classical linear logic have multisets rather than formulas as conclusions, thus a sequent calculus style notation will be used for them. The additive connectives are context-dependent and in order to avoid higher-order rules (as used for intuitionistic implication in Schroeder-Heister 1984) we give for the additive conjunction & two general elimination rules, and, dually, for the additive disjunction ⊕ two general introduction rules. The rules for the constants 1, ⊤, 0, ⊥ are obtained as nullary cases from the rules for ⊗, &, ⊕,^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , respectively. There are general introduction and elimination rules also for the modalities !,?. The calculus thus obtained is complete for classical linear logic.

The calculus is called a uniform calculus for the reason that it encompasses both natural deduction and sequent calculus, the rules of which are obtained as special instances. Natural deduction rules are obtained when the major premisses of introduction rules are assumptions (and thus deleted). Sequent calculus rules are obtained when also the major premisses of elimination rules are assumptions (and thus deleted).

Instances of the rules of the uniform calculus with minor premisses assumptions give all the invertibilities and partial invertibilities for the sequent calculus rules of linear logic. By restricting all the rules to their single-succedent versions, a uniform calculus, complete for intuitionistic linear logic, is obtained, and from this the corresponding sequent calculus (with its invertibilities) and natural deduction formulations.

The uniform calculus can be given in two forms, namely with explicit or implicit structural rules. In the latter form, the modalities have an introduction and elimination rule only, both justified by the inversion principles. The rules of !-weakening and !-contraction are derivable from the introduction and elimination rules for !, and analogously for the modality ?.

A derivation in the uniform calculus is in normal form when all its major premisses are assumptions. For the version of the uniform calculus with implicit structural rules the definition of normal derivation is modified by the requirement that all instances of the rules for the modalities are of a prescribed form. Normalization and the subformula property for normal derivations are proved through translation to sequent calculus, cut elimination, and translation back to the uniform calculus.

2. Inversion principles and the justification of the logical rules

In order to maintain the exposition self-contained we repeat here some background on the use of general elimination rules in natural deduction. General elimination rules for intuitionistic logic were introduced in von Plato (2001, see also von Plato 2000). A thorough exposition of natural deduction with general elimination rules can be found in Negri and von Plato (2001).

Introduction rules are usually justified in proof-theoretical terms through the BHK-interpretation of logical constants, which gives the sufficient grounds for deriving a formula. General elimination rules can then be obtained from the introduction rules through an inversion principle: Whatever follows from the grounds for deriving a formula must follow from that formula.

Whereas Prawitz’ inversion principle only justifies the elimination rules, this stronger inversion principle determines the elimination rules, once the introduction rules are given. For instance, given the introduction rule for conjunction

\begin{matrix}⋮ . ; A & ⋮ . ; B \\ A ∧ B \end{matrix} ^{∧I}

through the inversion principle the elimination rule is determined: The grounds for asserting A ∧ B are (derivations of) A and B, one obtains the rule

\begin{matrix}⋮ . ; A ∧ B & [A, B] ; ⋮ . ; C \\ C \end{matrix}_{∧E}

By writing out the multisets of open assumptions and replacing the vertical dots with the symbol for the formal derivability relation →, the two rules above read as

\begin{matrix}Γ → A & Δ → B \\ Γ, Δ → A ∧ B \end{matrix} ^{∧I}  \begin{matrix}Γ → A ∧ B & A, B, Δ → C \\ Γ, Δ → C \end{matrix} ^{∧E}

The conjunction elimination rules in their standard form

{Γ → A ∧ B \atop Γ → A} ^{∧E_{1}}  {Γ → A ∧ B \atop Γ → B} ^{∧E_{2}}

are obtained as special cases from ∧E when C is A or B, respectively, with the second premiss derivable. The general elimination rule for ∧ was first given for a system of intuitionistic logic in Schroeder-Heister (1984).

General elimination rules have already been used, to some extent, in linear logic. They have been given for ⊕, analogously to the elimination rule for disjunction, and for ⊗: These choices were wellnigh inevitable, the first due to the meaning of disjunction, the second due to the fact that one cannot project from A ⊗ B as from A&B. Following type theory in the design of a logical calculus, general elimination rules for ⊗, &, and ⊕ have been given in Valentini (1992).

A derivation of B from A gives the sufficient grounds for deriving an implication A ⊃ B. Therefore, in the formulation of the general elimination rule for implication we should have to express that something follows from a derivation, but there is no way to do this unless with the use of higher-level rules, as in Schroeder-Heister (1984). On the other hand a satisfactory solution in first-order logic is obtained by noting that if A ⊃ B holds, arbitrary consequences of B are already consequences of A. With this proviso, the general implication elimination rule for intuitionistic logic is formulated as

\begin{matrix}Γ → A ⊃ B & Δ → A & B, Π → C \\ Γ, Δ, Π → C \end{matrix} ^{⊃E}

varlin.tex; 14/06/2002; 12:44; p.5

which replaces the special implication elimination rule of modus ponens

\begin{matrix}Γ → A ⊃ B & Δ → A \\ Γ, Δ → B \end{matrix} ^{⊃E}

obtained when B = C. It seems that the general elimination rule for implication was first presented in Dyckhoff (1988).

The general elimination rule for linear implication is the same as for intuitionistic implication:

\begin{matrix}Γ → A ⊸ B & Δ → A & B, Π → C \\ Γ, Δ, Π → C \end{matrix} ^{⊸E}

Determining the rules for the context-dependent connectives, or additives, is not completely straightforward: The grounds for obtaining A&B are derivations of A and B from the same multiset of open assumptions. Again, this would bring to a higher-level condition in the elimination rules, not expressible in first-order logic. The two, instead of one, elimination rules for the additive conjunction are a way to overcome this problem:

\begin{matrix}Γ → A&B & A, Δ → C \\ Γ, Δ → C \end{matrix} ^{&E_{1}}  \begin{matrix}Γ → A&B & B, Δ → C \\ Γ, Δ → C \end{matrix} ^{&E_{2}}

The standard elimination rules of natural deduction (special elimination rules), are obtained as special cases of the general elimination rules. As seen above for modus ponens, also the special elimination rules for & follows from the general elimination rule when the right premiss is an axiom A → A or B → B. Modus ponens is similarly an instance of the general implication elimination rule.

By using special elimination rules there is no obvious correspondence between normal derivations in natural deduction and cut-free derivations in sequent calculus. The translation of a step of &E_{1}

{Γ → A&B \atop Γ → A} ^{&E_{1}}

is the following

\begin{matrix}Γ ⇒ A&B & {A ⇒ A \atop A&B ⇒ A} ^{L&_{1}} \\ Γ ⇒ A \end{matrix}_{cut}

where an extra cut is needed. In the converse translation from sequent calculus to natural deduction a step of L&_{1}

{A, Γ ⇒ C \atop A&B, Γ ⇒ C} ^{L&_{1}}

varlin.tex; 14/06/2002; 12:44; p.6

becomes

\begin{matrix}{A&B → A&B \atop A&B → A} ^{&E_{1}} & A, Γ → C \\ A&B, Γ → C \end{matrix} ^{subst}

with a possible non-normality produced by the step of substitution^{1}.

By using general elimination rules no cut is introduced in the translation from normal natural deduction to sequent calculus, and no nonnormalities arise in a translation of cut-free derivations.

In the rules of the uniform calculus, the major premiss is the premiss containing the connective or the constant of the rule in question. The other premisses are called minor premisses.

General introduction rules are dual to general elimination rules: The principal formula appears in the antecedent of the major premisses, whereas in general elimination rules the principal formula appears in the succedent of the major premiss. The semantical justification for general introduction rules can be given in terms of a dual inversion principle: Whatever follows from a formula must follow from the sufficient grounds for deriving the formula.

A couple of examples illustrate how the dual inversion principle determines the general introduction rules.

1. The sufficient grounds for deriving A⊕B are given by a derivation of A or a derivation of B. By the dual inversion principle, whatever follows from A ⊕ B must follow from A and whatever follows from A ⊕ B must follow from B, thus we get the rules

\begin{matrix}[A ⊕ B] ; ⋮ . ; C & ⋮ . ; A \\ C \end{matrix} ^{⊕I_{1}}  \begin{matrix}[A ⊕ B] ; ⋮ . ; C & ⋮ . ; B \\ C \end{matrix} ^{⊕I_{2}}

With the multisets of assumptions written out explicitly and a sequentstyle notation, we obtain the rules

\begin{matrix}A ⊕ B, Γ → C & Δ → A \\ Γ, Δ → C \end{matrix} ^{⊕I_{1}}  \begin{matrix}A ⊕ B, Γ → C & Δ → B \\ Γ, Δ → C \end{matrix} ^{⊕I_{2}}

2. The sufficient grounds for deriving A ⊸ B are given by a derivation of B from A. The dual inversion principle thus gives the rule, in either notation

\begin{matrix}[A ⊸ B] ; ⋮ . ; C & A ; ⋮ . ; B \\ C \end{matrix} ^{⊸I}  \begin{matrix}A ⊸ B, Γ → C & A, Δ → B \\ Γ, Δ → C \end{matrix} ^{⊸I}

The rules for all the other connectives are obtained in a similar fashion.

varlin.tex; 14/06/2002; 12:44; p.7

3. The uniform calculus and its basic properties

The most general version of the uniform calculus is the one for classical linear logic. It has multiple conclusion rules, thus in the inversion principles arbitrary conclusions are given by a multiset of formulas rather than a single formula.

By the method described in the previous section the introduction and elimination rules of the uniform calculus for ⊗, &, ⊕, and ⊸ are found. The rules for ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} are dual to the rules for ⊗.

The rules for the constants 1, ⊤, 0, and ⊥ are found as degenerate instances of the rules for the connectives of which these constants are the unit elements: First the rule for the matching connective is generalized to a finite arity, then the empty instance is taken. For example, rule &I generalized to n conjuncts is the rule with n + 1 premisses

&_{1≤i≤n}A_{i}, Γ → Δ {Γ′ → Δ′, A_{i}}_{1≤i≤n}
Γ, Γ′ → Δ, Δ′

which gives, for n = 0

{⊤, Γ → Δ \atop Γ, Γ′ → Δ, Δ′}

The generalization of &E to n conjuncts is given by the n two-premiss rules

Γ → Δ, &_{1≤i≤n}A_{i} A_{i}, Γ′ → Δ′
Γ, Γ′ → Δ, Δ′

for each i such that 1 ≤ i ≤ n. For n = 0 no rule is produced, so there cannot be a rule of elimination for ⊤. The rules for the other constants are found similarly, and the syntactic impossibility for a rule of 0-introduction is shown.

The calculus has only one axiom, A → A, which corresponds to the rule of assumption in natural deduction. For this reason, a premiss is called an assumption if it is of the form A → A.

The rules for the modalities !, ? are also justified by means of the inversion principles. The grounds for deriving !A are given by a derivation of A from !-assumptions. In the presence of multiple-conclusion, A can be accompanied by ?-alternatives, so rule ?I is justified. For !E we cannot encode the grounds for deriving !A without a higher order syntax, but we use what is a sufficient ground for deriving !A, namely having A without assumptions. So the rule becomes the formal transcription of the inversion principle thus instantiated: Whatever follows from A must follow from !A.

Rules ?I and ?E are obtained by symmetry from !E and !I, respectively.

The structural rules for the modality ! follow the pattern of general elimination rules, where a multiplicity rather than a formula is eliminated. The structural rules for ? instead follow the pattern of general introduction rules. None of these structural rules has a direct explanation in terms of the inversion principles. However, they can be dispensed with through a natural generalization of the introduction or elimination rules for the modalities, as we shall see below.

Uniform calculus for classical linear logic Ucl

Axiom

A → A

Rules for ⊗, &, ⊕, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , ⊸

A ⊗ B, Γ → Δ Γ′ → Δ′, A Γ′′ → Δ′′, B

Γ, Γ′, Γ′′ → Δ, Δ′, Δ′′ ⊗I

Γ → Δ, A ⊗ B A, B, Γ′ → Δ′

Γ, Γ′ → Δ, Δ′ ⊗E

A&B, Γ → Δ Γ′ → Δ′, A Γ′ → Δ′, B

Γ, Γ′ → Δ, Δ′ &I

Γ → Δ, A&B A, Γ′ → Δ′ Γ, Γ′ → Δ, Δ′ ^{&E_{1}}  Γ → Δ, A&B B, Γ′ → Δ′ Γ, Γ′ → Δ, Δ′ ^{&E_{2}}
A ⊕ B, Γ → Δ Γ′ → Δ′, A Γ, Γ′ → Δ, Δ′ ^{⊕I_{1}}  A ⊕ B, Γ → Δ Γ′ → Δ′, B Γ, Γ′ → Δ, Δ′ ^{⊕I_{2}}
Γ → Δ, A ⊕ B A, Γ′ → Δ′ B, Γ′ → Δ′

Γ, Γ′ → Δ, Δ′ ⊕E

A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B, Γ → Δ Γ′ → Δ′, A, B

Γ, Γ′ → Δ, Δ′ .^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} I

Γ → Δ, A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B A, Γ′ → Δ′ B, Γ′′ → Δ′′

Γ, Γ′, Γ′′ → Δ, Δ′, Δ′′ .^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} E

A ⊸ B, Γ → Δ A, Γ′ → Δ′, B

Γ, Γ′ → Δ, Δ′ ⊸I

Γ → Δ, A ⊸ B Γ′ → Δ′, A B, Γ′′ → Δ′′

Γ, Γ′, Γ′′ → Δ, Δ′, Δ′′ ⊸E

varlin.tex; 14/06/2002; 12:44; p.9

Rules for 1, ⊤, 0, ⊥

{1, Γ → Δ \atop Γ → Δ} ^{1I}  Γ → Δ, 1 Γ′ → Δ′ Γ, Γ′ → Δ, Δ′ ^{1E}
{⊤, Γ → Δ \atop Γ, Γ′ → Δ, Δ′} ^{⊤I}  no elimination rule for ⊤
no introduction rule for 0  {Γ → Δ, 0 \atop Γ, Γ′ → Δ, Δ′} ^{0E}
⊥, Γ → Δ Γ′ → Δ′ Γ, Γ′ → Δ, Δ′ ^{⊥I}  {Γ → Δ, ⊥ \atop Γ → Δ} ^{⊥E}

Rules for !, ?

!A, Γ → Δ !Γ′ →?Δ′, A Γ,!Γ′ → Δ,?Δ′ ^{!I}  Γ → Δ,!A A, Γ′ → Δ′ Γ, Γ′ → Δ, Δ′ ^{!E}
?A, Γ → Δ Γ′ → Δ′, A Γ, Γ′ → Δ, Δ′ ^{?I}  Γ → Δ,?A A,!Γ′ →?Δ′ Γ,!Γ′ → Δ,?Δ′ ^{?E}
Γ → Δ,!A Γ′ → Δ′ Γ, Γ′ → Δ, Δ′ ^{!w}  !Γ →?Δ,!A !A,!A, Γ′ → Δ′ !Γ, Γ′ →?Δ, Δ′ ^{!c}
?A, Γ → Δ Γ′ → Δ′ Γ, Γ′ → Δ, Δ′ ^{?w}  ?A,!Γ →?Δ Γ′ → Δ′,?A,?A !Γ, Γ′ →?Δ, Δ′ ^{?c}

The first basic property of the uniform calculus is closure under substitution:

Proposition 3.1 The rule of substitution

Γ → Δ, C C, Π → Φ
Γ, Π → Δ, Φ

subst

is admissible in Ucl.

Proof: By induction on the sum of the heights of the derivations of the two premisses. If one of the premisses is an axiom, the conclusion is given by the other premiss, and there is nothing to prove. Else both premisses are derived by some rule. Consider the derivation of the right premiss. If the last rule is any rule except one of the context-dependent rules !I, ?E, !c or ?c, we observe that substitution can be permuted up to the premiss(es) where C appears, and the conclusion is obtained by applying the same rule to the premisses thus obtained. A similar permutation can be performed if C appears in the left premiss of !I, ?E, !c, or ?c, since the left premiss of these rules is context-independent. If C appears instead in the right premiss of, say, !I, C is of the form !B for some formula B. Consider now the last rule R in the derivation of Γ → Δ, C. If R is not !I ?E, !c, or ?c, we proceed by permuting substitution to the premiss(es) of R. Else, if R if !I, ?E, !c, or ?c, since the formula C is an !-formula it cannot belong to the context-dependent premiss of these rules, which have a context made of ?-formulas as succedent. Thus substitution can be permuted. A similar reasoning applies in all other critical cases, where the last rule used to derive C, Π → Φ is ?E, !c, or ?c and C appears in the left premiss of these rules.

The calculus above can be simplified to one where both modalities have only an introduction and an elimination rule, by considering the following generalizations of !E and ?I, where n = 0, 1, 2, …

Γ → Δ,!A A^{n}, Γ′ → Δ′ Γ, Γ′ → Δ, Δ′ ^{!E^{∗}}  ?A, Γ → Δ Γ′ → Δ′, A^{n} Γ, Γ′ → Δ, Δ′ ^{?I^{∗}}

By using the above rules, the structural rules of weakening and contraction become derivable:

Proposition 3.2 Rules !w and !c are derivable from !E^{∗} and !I. Rules ?w and ?c are derivable from ?I^{∗} and ?E. Proof: Observe that !w is just the instance of !E^{∗} where n = 0. Similarly, ?w is the instance of ?I^{∗} with n = 0. Rules !c and ?c are derived as follows:

\begin{matrix}!!A →!!A & !Γ →?Δ,!A \\ !Γ →?Δ,!!A \end{matrix} ^{!I} !A,!A, Γ′ → Δ′

!Γ, Γ′ →?Δ, Δ′ !E^{∗}

\begin{matrix}??A →??A & ?A,!Γ →?Δ \\ ??A,!Γ →?Δ \end{matrix} ^{?E} Γ′ → Δ′,?A,?A

!Γ, Γ′ →?Δ, Δ′ ?I^{∗}

Alternatively, instead of generalizing the rules of !-introduction and ?-elimination, the rules of !-elimination and ?-introduction can be generalized so that weakening and contraction are derivable. Consider the following rules, where n = 0, 1, 2, …

!A^{n}, Γ → Δ !Γ′ →?Δ′, A Γ,!Γ′ → Δ,?Δ′ ^{!I^{∗}}  Γ → Δ,?A^{n} A,!Γ′ →?Δ′ Γ,!Γ′ → Δ,?Δ′ ^{?E^{∗}}

Then we have:

Proposition 3.3 Rules !w and !c are derivable from !I^{∗} and !E. Rules ?w and ?c are derivable from ?I and ?E^{∗}.

Proof: The rules of weakening for !- and ?-formulas are derived as follows:

Γ → Δ,!A \begin{matrix}Γ′ → Δ′ & \begin{matrix}!A →!A & A → A \\ !A → A \end{matrix} ^{!E} \\ !A, Γ′ → Δ′ \end{matrix}_{!I^{∗} (n=0)}
Γ, Γ′ → Δ, Δ′

subst

\begin{matrix}Γ′ → Δ′ & \begin{matrix}?A →?A & A → A \\ A →?A \end{matrix} ^{?I} \\ Γ′ → Δ′,?A \end{matrix}_{?E^{∗} (n=0)} ?A, Γ → Δ
Γ, Γ′ → Δ, Δ′

subst

Rules !c and ?c are derivable by

!A,!A, Γ′ → Δ′ \begin{matrix}!Γ →?Δ,!A & A → A \\ !Γ →?Δ, A \end{matrix} ^{!E}

!Γ, Γ′ →?Δ, Δ′ !I^{∗}

\begin{matrix}?A,!Γ →?Δ & A → A \\ A,!Γ →?Δ \end{matrix} ^{?I} Γ′ → Δ′,?A,?A

!Γ, Γ′ →?Δ, Δ′ ?E^{∗}

Observe that in the proof above substitution cannot be removed until both its premisses are replaced by “concrete” derivations.

Definition 3.4 Let Ucl^{∗} be the calculus obtained from Ucl by replacing the rules !E and ?I with !E^{∗} and ?I^{∗} and by removing the rules !w, !c, ?w, and !c.

Let Ucl_{∗} be the calculus obtained from Ucl by replacing the rules !I and ?E with !I^{∗} and ?E^{∗} and by removing the rules !w, !c, ?w, and !c.

By the proof of proposition 3.1 it follows that the rule of substitution is also admissible for the calculi Ucl^{∗} and Ucl_{∗}.

By Propositions 3.2 and 3.3 both of the calculi Ucl^{∗} and Ucl_{∗} are equivalent to Ucl and all are complete for classical linear logic.

4. The varieties of linear calculi generated by the uniform calculus

Formally, the uniform calculus can be described as a multiple conclusion natural deduction system with general introduction and general elimination rules, written in sequent calculus style. The uniform calculus thus encompasses features of both natural deduction and sequent calculus. Systems of natural deduction and sequent calculus for classical and intuitionistic linear logic can be obtained from the uniform calculus as special cases.

4.1. From the uniform calculus to sequent calculus and its inversions

By instantiating the major premisses of the rules of Ucl to a (derivable) premiss of the form A ∘ B → A ∘ B, where ∘ is a binary connective, or to the form μA → μA, where μ is ! or ?, we obtain the familiar sequent calculus rules for classical linear logic. For instance, by taking Γ to be the empty (multi)set and Δ ≡ A ⊗ B in the rule ⊗I, we obtain

A ⊗ B → A ⊗ B Γ′ → Δ′, A Γ′′ → Δ′′, B
Γ′, Γ′′ → Δ′, Δ′′, A ⊗ B

Since the left premiss is derivable, this rule is equivalent to

Γ′ → Δ′, A Γ′′ → Δ′′, B
Γ′, Γ′′ → Δ′, Δ′′, A ⊗ B

which is the usual R⊗. In a similar way, the other rules are obtained. The full table of rules of the calculus Gcl, given below, presents each rule in the position corresponding to the rule of the uniform calculus from which it is derived. The calculus we obtain is the same as the calculus often called CLL in the literature (cf. Troelstra 1992, where a different notation and rules for primitive negation are used).

Sequent calculus for classical linear logic Gcl

Axiom

A ⇒ A

Rules for ⊗, &, ⊕, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , ⊸:

Γ ⇒ Δ, A Γ′ ⇒ Δ′, B Γ, Γ′ ⇒ Δ, Δ′, A ⊗ B ^{R⊗}  {A, B, Γ ⇒ Δ \atop A ⊗ B, Γ ⇒ Δ} ^{L⊗}
\begin{matrix}Γ ⇒ Δ, A & Γ ⇒ Δ, B \\ Γ ⇒ Δ, A&B \end{matrix} ^{R&}  {A, Γ ⇒ Δ \atop A&B, Γ ⇒ Δ} ^{L&_{1}}  {B, Γ ⇒ Δ \atop A&B, Γ ⇒ Δ} ^{L&_{2}}
{Γ ⇒ Δ, A \atop Γ ⇒ Δ, A ⊕ B} ^{R⊕_{1}}  {Γ ⇒ Δ, B \atop Γ ⇒ Δ, A ⊕ B} ^{R⊕_{2}}  \begin{matrix}A, Γ ⇒ Δ & B, Γ ⇒ Δ \\ A ⊕ B, Γ ⇒ Δ \end{matrix} ^{L⊕}
{Γ ⇒ Δ, A, B \atop Γ ⇒ Δ, A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B} ^{R^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}  A, Γ ⇒ Δ B, Γ′ ⇒ Δ′ A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B, Γ, Γ′ ⇒ Δ, Δ′ ^{L^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}
{A, Γ ⇒ Δ, B \atop Γ ⇒ Δ, A ⊸ B} ^{R⊸}  Γ ⇒ Δ, A Γ′ ⇒ Δ′, B A ⊸ B, Γ, Γ′ ⇒ Δ, Δ′ ^{L⊸}

varlin.tex; 14/06/2002; 12:44; p.13

Rules for 1, ⊤, 0, ⊥

⇒ 1 ^{R1}  {Γ ⇒ Δ \atop 1, Γ ⇒ Δ} ^{L1}
Γ ⇒ Δ, ⊤ ^{R⊤}
0, Γ ⇒ Δ ^{L0}
{Γ ⇒ Δ \atop Γ ⇒ Δ, ⊥} ^{R⊥}  ⊥ ⇒ ^{L⊥}

Rules for !, ?

{!Γ ⇒?Δ, A \atop !Γ ⇒?Δ,!A} ^{R!}  {A, Γ ⇒ Δ \atop !A, Γ ⇒ Δ} ^{L!}
{Γ ⇒ Δ, A \atop Γ ⇒ Δ,?A} ^{R?}  {A, Γ ⇒ Δ \atop ?A,!Γ ⇒?Δ} ^{L?}
{Γ ⇒ Δ \atop !A, Γ ⇒ Δ} ^{L-weak}  {!A,!A, Γ ⇒ Δ \atop !A, Γ ⇒ Δ} ^{L-contr}
{Γ ⇒ Δ \atop Γ ⇒ Δ,?A} ^{R-weak}  {Γ ⇒ Δ,?A,?A \atop Γ ⇒ Δ,?A} ^{R-contr}

By taking instances of the rules of the uniform calculus where minor premisses are assumptions, we obtain all the invertibilities of the sequent calculus for classical linear logic. For instance, instantiating in ⊗I, Γ′ with A, Γ′′ with B and Δ′, Δ′′ with the empty multi(set) we obtain

\begin{matrix}A ⊗ B, Γ ⇒ Δ & A ⇒ A & B ⇒ B \\ A, B, Γ ⇒ Δ \end{matrix}

Since the two minor premisses are derivable, this rule amounts to

{A ⊗ B, Γ ⇒ Δ \atop A, B, Γ ⇒ Δ}

which is invertibility of L⊗.

In some cases there is no special instance where the minor premisses are axioms. This happens when the minor premiss contains two active formulas, namely for the rules ⊗E, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} I, !c and ?c and when there is no minor premiss, such as in 1I, ⊤I, 0E and ⊥E. Correspondingly, there is no inversion for R⊗, L^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , L-contr, R-contr (although the inverses of the two latter are instances of the rules L-weak, R-weak) nor for L1 or R⊥. In other cases an instance where the minor premisses are axioms is produced only by imposing active formulas to have a certain form. This happens for the context sharing rules &I, ⊕E and for ⊸ I and for the context-sensitive rules !I and ?E. In these cases there are special inversions.

Observe that some of these inversions are known already (cf. Prop. 3.7 in Troelstra 1992). What is peculiar here is that there is no need of any metatheoretical argument, like induction on derivations, for obtaining them, but they are automatically generated from the uniform calculus.

In the table below of inversions for Gcl, the position of each inversion is the same as in the table of the corresponding rule of the uniform calculus from which it is obtained. The name instead indicates the rule of sequent calculus to which it pertains.

Observe that rules without minor premisses do not have any corresponding inversions. In some cases there are odd-looking inversions, namely those obtained from 1E, ⊥I, !w and ?w: In all these cases the conclusion is of the form of a generalized axiom C, Γ ⇒ Δ, C, where C is an arbitrary formula.

Inversions for Gcl

Inversions for ⊗, &, ⊕, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , ⊸

{A ⊗ B, Γ ⇒ Δ \atop A, B, Γ ⇒ Δ} ^{L⊗-inv}  no inversion for R⊗
{A&A, Γ ⇒ Δ \atop A, Γ ⇒ Δ} ^{L&-inv}  {Γ ⇒ Δ, A&B \atop Γ ⇒ Δ, A} ^{R&-inv_{1}}  {Γ ⇒ Δ, A&B \atop Γ ⇒ Δ, B} ^{R&-inv_{2}}
{A ⊕ B, Γ ⇒ Δ \atop A, Γ ⇒ Δ} ^{L⊕-inv_{1}}  {A ⊕ B, Γ ⇒ Δ \atop B, Γ ⇒ Δ} ^{L⊕-inv_{2}}  {Γ ⇒ Δ, A ⊕ A \atop Γ ⇒ Δ, A} ^{R⊕-sp.inv}
no inversion for L^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  {Γ ⇒ Δ, A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B \atop Γ ⇒ Δ, A, B} ^{R^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} -inv}
{A ⊸ A, Γ ⇒ Δ \atop Γ ⇒ Δ} ^{L⊸-sp.inv}  {Γ ⇒ Δ, A ⊸ B \atop A, Γ ⇒ Δ, B} ^{R⊸-inv}

Inversions for 1, ⊤, 0, ⊥:

no inv. for L1  {Γ ⇒ Δ, 1 \atop C, Γ ⇒ Δ, C} ^{R1-inv}
{⊥, Γ ⇒ Δ \atop C, Γ ⇒ Δ, C} ^{L⊥-inv}  no inv. for R⊥

Inversions for !, ?:

{!!A, Γ ⇒ Δ \atop !A, Γ ⇒ Δ} ^{L!-sp.inv}  {Γ ⇒ Δ,!A \atop Γ ⇒ Δ} ^{R!−inv}
{?A, Γ ⇒ Δ \atop A, Γ ⇒ Δ} ^{L?−inv}  {Γ ⇒ Δ,??A \atop Γ ⇒ Δ,?A} ^{R?-sp.inv}

varlin.tex; 14/06/2002; 12:44; p.15

4.2. From the uniform calculus to sequent calculus and natural deduction for intuitionistic linear logic

By restricting the uniform calculus for classical linear logic to its singlesuccedent version we obtain a uniform calculus for intuitionistic linear logic, Uil. The table of rules is the following:

Uniform calculus for intuitionistic linear logic Uil

Axiom

A → A

Rules for ⊗, &, ⊕, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , ⊸:

\begin{matrix}A ⊗ B, Γ → C & Γ′ → A & Γ′′ → B \\ Γ, Γ′, Γ′′ → Δ \end{matrix} ^{⊗I}  \begin{matrix}Γ → A ⊗ B & A, B, Γ′ → C \\ Γ, Γ′ → C \end{matrix} ^{⊗E}
\begin{matrix}A&B, Γ → C & Γ′ → A & Γ′ → B \\ Γ, Γ′ → C \end{matrix} ^{&I}
\begin{matrix}Γ → A&B & A, Γ′ → C \\ Γ, Γ′ → C \end{matrix} ^{&E_{1}}  \begin{matrix}Γ → A&B & B, Γ′ → C \\ Γ, Γ′ → C \end{matrix} ^{&E_{2}}
\begin{matrix}A ⊕ B, Γ → C & Γ′ → A \\ Γ, Γ′ → C \end{matrix} ^{⊕I_{1}}  \begin{matrix}A ⊕ B, Γ → C & Γ′ → B \\ Γ, Γ′ → C \end{matrix} ^{⊕I_{2}}
\begin{aligned}Γ → A ⊕ B & A, Γ′ → C & B, Γ′ → C \\ & Γ, Γ′ → C \end{aligned} ^{⊕E}
\begin{matrix}A ⊸ B, Γ → C & A, Γ′ → B \\ Γ, Γ′ → C \end{matrix} ^{⊸I}  \begin{matrix}Γ → A ⊸ B & Γ′ → A & B, Γ′′ → C \\ Γ, Γ′, Γ′′ → C \end{matrix} ^{⊸E}

Rules for 1, ⊤, 0

{1, Γ → C \atop Γ → C} ^{1I}  \begin{matrix}Γ → 1 & Γ′ → C \\ Γ, Γ′ → C \end{matrix} ^{1E}
{⊤, Γ → C \atop Γ, Γ′ → C} ^{⊤I}  no elimination rule for ⊤
no introduction rule for 0  {Γ → 0 \atop Γ, Γ′ → C} ^{0E}

Rules for !

\begin{matrix}!A, Γ → C & !Γ′ → A \\ Γ,!Γ′ → C \end{matrix} ^{!I}  \begin{matrix}Γ →!A & A, Γ′ → C \\ Γ, Γ′ → C \end{matrix} ^{!E}
\begin{matrix}Γ →!A & Γ′ → C \\ Γ, Γ′ → C \end{matrix} ^{!w}  \begin{matrix}!Γ →!A & !A,!A, Γ′ → C \\ !Γ, Γ′ → C \end{matrix} ^{!c}

varlin.tex; 14/06/2002; 12:44; p.16

In a way completely similar to what we have done for Ucl, one obtains from Uil the usual sequent calculus for intuitionistic linear logic, often called ILL in the literature, and its inversions.

For a natural deduction system, we have the possibility of some choices, namely, we can specialize all the rules of the uniform calculus to their special form, and obtain a system of natural deduction that resembles the one for intuitionistic logic, or we can just specialize the introduction rules, and obtain a system of natural deduction with general elimination rules. Special instances of introduction rules are obtained by considering the case when the major premiss is an assumption. Special instances of elimination rules are instead obtained by considering the cases when the minor premisses are assumptions, whenever this is applicable (for instance, it is not for ⊗E, so the rule of elimination for ⊗ can be formulated only in a general form). For &E_{1} the instance with minor premiss an assumption is

\begin{matrix}Γ → A&B & A → A \\ Γ → A \end{matrix}

by deleting the derivable premiss A → A this is equivalent to the rule

{Γ → A&B \atop Γ → A}

which is the usual special elimination rule for &. The other special elimination rules for all connectives are obtained similarly.

A system of natural deduction for intuitionistic linear logic with general elimination rules is studied in Negri 2002, thus we shall not investigate it here any further, but just limit ourselves to observing that it is obtained, as the previous systems, as a special case of the uniform calculus.

5. Normalization

In this section we shall give a proof of normalization for the uniform calculus Ucl. For the uniform calculi with in-built weakening and contraction, Ucl^{∗} and Ucl_{∗}, the definition of normal derivation will have to be slightly modified. We recall the following:

Definition 5.1 In each rule of the uniform calculi Ucl, the major premiss is the premiss containing the logical constant of the rule. The other premisses are called minor premisses. A premiss is an assumption if it is of the form A → A.

Definition 5.2 A derivation in Ucl is in normal form if all the major premisses are assumptions.

For the uniform calculus with implicit weakening and contraction the definition of normal derivation has to be modified so as to include those instances of !I^{∗}, ?E^{∗} or !E^{∗}, ?I^{∗} that correspond to weakening and contraction for !,?-formulas.

For the calculus Ucl^{∗} the definition of normality needs to be modified by the following:

Definition 5.3 An instance of !E^{∗} is simple if its major premiss is an assumption or it is of the form !A →!!A. An instance of ?I^{∗} is simple if its major premiss is an assumption or it is of the form ??A →?A. A derivation in Ucl^{∗} is in normal form if all the major premisses of rules other than !E^{∗}, ?I^{∗} are assumptions and all instances of !E^{∗}, ?I^{∗} are simple.

A similar modification is needed for the definition of normality for the system Ucl_{∗}:

Definition 5.4 An instance of !I^{∗} is simple if its major premiss is an assumption or if its minor premiss is of the form !A → A. An instance of ?E^{∗} is simple if its major premiss is an assumption or if its minor premiss is of the form A →?A. A derivation in Ucl_{∗} is in normal form if all the major premisses of rules other than !I^{∗}, ?E^{∗} are assumptions and all instances of !I^{∗}, ?E^{∗} are simple.

The proof of normalization for the uniform calculus is obtained by a translation between sequent calculus and the uniform calculus such that cut-free derivations in sequent calculus correspond to normal derivation in the uniform calculus. Cut-elimination for sequent calculus then yields the result.

The translation S from the uniform calculus to sequent calculus is defined by induction on the derivation tree. Axiom A → A is translated by A ⇒ A. A derivation ending with an introduction rule is translated via the corresponding right rule of sequent calculus and cut and one ending with an elimination rule via the corresponding left rule and cut, as follows:

A ⊗ B, Γ → Δ^{π} Γ′ → Δ′, A^{π_{1}} Γ′′ → Δ′′, B^{π_{2}}

Γ, Γ′, Γ′′ → Δ, Δ′, Δ′′ ⊗I

is translated as

Γ′ ⇒ Δ′, A^{S(π_{1})} Γ′′ ⇒ Δ′′, B^{S(π_{2})} Γ, Δ ⇒ A ⊗ B ^{R⊗} A ⊗ B, Γ ⇒ Δ^{S(π)}

Γ, Γ′, Γ′′ → Δ, Δ′, Δ′′ cut

varlin.tex; 14/06/2002; 12:44; p.18

Γ → Δ, A ⊗ B^{π_{1}} A, B, Γ′ → Δ′^{π_{2}}

Γ, Γ′ → Δ, Δ′ ⊗E

is translated as

Γ ⇒ Δ, A ⊗ B^{S(π_{1})} A, B, Γ′ ⇒ Δ′^{S(π_{2})} ; A ⊗ B, Γ′ ⇒ Δ′ ^{L⊗}

Γ, Γ′ ⇒ Δ, Δ′ cut

All the other rules are translated in a similar way. Observe that no cut is needed in the translation of normal instances of rules.

The translation of the rules !I^{∗}, ?E^{∗}, !E^{∗}, and ?I^{∗} has steps of weakening and contraction with n as parameter. No cut is needed in the translation of simple instances of these rules.

We have thus proved:

Proposition 5.5 Given a derivation D in Ucl, Ucl^{∗}, or Ucl_{∗}, its translation S(D) is a derivation in Gcl + cut. If D is in normal form, its translation is a derivation in Gcl.

The translation N from sequent calculus to the uniform calculus is also defined inductively, starting with the translation of the axioms and proceeding with the translation of the sequent calculus rules. For instance, the rules for ⊸ are translated as follows: a step of the form

A, Γ ⇒ Δ, B^{d} ; Γ ⇒ Δ, A ⊸ B ^{R⊸}

becomes

\begin{matrix}A ⊸ B → A ⊸ B & A, Γ → Δ, B^{N(d)} \\ Γ → Δ, A ⊸ B \end{matrix} ^{⊸I}

and

\begin{matrix}Γ ⇒ A^{d_{1}} & B, Δ ⇒ Δ^{d_{2}} \\ A ⊸ B, Γ, Δ ⇒ Δ \end{matrix} ^{L⊸}

becomes

A ⊸ B → A ⊸ B Γ → A^{N(d_{1})} B, Δ → Δ^{N(d_{2})}

A ⊸ B, Γ, Δ → Δ ⊸E

In a similar way all the other rules are translated into rules of the uniform calculus where major premisses are assumptions. The translations to the uniform calculi with implicit weakening and contraction are obtained by modifying the translation of the structural rules only. The rules of weakening and contraction are translated into simple instances of the starred !-? rules. We shall denote by N^{∗} the translation to Ucl^{∗} and by N_{∗} the translation to Ucl_{∗}.

Proposition 5.6 Given a derivation d in Gcl + cut, its translation N(d) (N^{∗}(d), N_{∗}(d) resp.) is a derivation in Ucl (Ucl^{∗}, Ucl_{∗} resp.) If d is cut free, its translation is a normal derivation.

By Propositions 5.5 and 5.6 and cut-elimination for Gcl we have:

Theorem 5.7 Every derivation in Ucl, Ucl^{∗}, or Ucl_{∗} can be transformed into a derivation in normal form.

By inspection on normal instances of the rules we have the following subformula properties:

Theorem 5.8 All formulas occurring in a normal derivation in Ucl or Ucl_{∗} are subformulas of the conclusion. All formulas occurring in a normal derivation in Ucl^{∗} are subformulas of the conclusion or !A, ?A for A subformula of the conclusion.

The same results hold, with obvious modifications, for the uniform calculus Uil and its variants without explicit weakening and contraction. It is also unproblematic to include the quantifiers in this treatment.

Notes

1. In Prawitz 1965 a translation between cut-free sequent calculus and normal natural deduction derivations is described. Contexts are treated as sets and the sequent calculus employed uses a non-invertible L∧ rule. The translation from sequent calculus to natural deduction translates right rules by natural deduction introduction rules that continue a proof tree from the bottom, whereas left rules are translated by natural deduction elimination rules that expand a proof tree from the leaves. A normal derivation, in Prawitz’ sense, is thus obtained. The reverse translation from natural deduction to sequent calculus implicitly uses steps of cut-elimination, in other words it is not an isomorphic translation. See also von Plato (2002) for a discussion on Prawitz’ translation. In a forthcoming work by Pfenning a translation between normal natural deduction and cut-free sequent calculus is presented in a fully formalized way. The translation from natural deduction to sequent calculus employs G3-like rules in order to take account of possible multiple use of assumptions in natural deduction.

References

Avellone, A., M. Ferrari and P. Miglioli (1999) Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics, Logic Journal of the IGPL, vol. 7, pp. 447–480.

Dyckhoff, R. (1988) Implementing a simple proof assistant, in Derrick and Lewis (eds), Proceedings of the Workshop on Programming for Logic Teaching, Leeds, 1987, Centre for Theoretical Computer Science and Departments of Pure Mathematics and Philosophy, Univ. of Leeds, no. 23.88, pp. 49–59.

Dyckhoff, R. and L. Pinto (1999) Permutability of proofs in intuitionistic sequent

calculi, Theoretical Computer Science, vol. 212, pp. 141–155. Herbelin, H. (1994) A λ calculus structure isomorphic to Gentzen-style sequent

calculus structure, in Pacholski and Tiuryn (eds), Lecture Notes in Computer Science, vol. 933, pp. 61–75.

Mints, G. (1996) Normal form of sequent derivations, in Odifreddi (ed) Kreiseliana,

A.K. Peters, pp. 469–492. Negri, S. (2002) A normalizing system of natural deduction for intuitionistic linear

logic, Archive for Mathematical Logic, in press. Negri, S. and J. von Plato. (2001) Structural Proof Theory, Cambridge University

Press. Negri, S. and J. von Plato. (2001a) Sequent calculus in natural deduction style The

Journal of Symbolic Logic, vol. 66, pp. 1803–1816. Pfenning, F. (2000) Personal communication. von Plato, J. (2000) A problem of normal form in natural deduction, Mathematical

Logic Quarterly, vol. 42, pp. 121-124. von Plato, J. (2001) Natural deduction with general elimination rules, Archive for

Mathematical Logic, vol. 40, pp. 541–567. von Plato, J. (2002) Translations from sequent calculus to natural deduction, Paper

presented at the conference Natural Deduction, Rio de Janeiro, July 2001. Prawitz, D. (1965) Natural Deduction, Almqvist and Wiksell, Stockholm. Schroeder-Heister, P. (1984) A natural extension of natural deduction, The Journal

of Symbolic Logic, vol. 49, pp. 1284–1300. Troelstra, A.S. (1992) Lectures on Linear Logic, CSLI Lecture Notes, no. 29, Stanford

University. Ungar, A. M. (1992) Normalization, cut-elimination and the theory of proofs, CSLI

Lecture Notes, no. 28, Stanford University. Valentini, S. (1992) The judgement calculus for intuitionistic linear logic: Proof

theory and semantics, Zeitschr. f. math. Logik und Grundlagen d. Math., vol. 38, pp. 39–58.

Address for Offprints: Sara Negri Department of Philosophy P.O. Box 9 00014 University of Helsinki Finland

varlin.tex; 14/06/2002; 12:44; p.22