On the Fine Structure of the Exponential Rule

Simone Martini Andrea Masini

Abstract

We present natural deduction systems for fragments of intuitionistic linear logic obtained by dropping weakening and contractions also on !-prefixed formulas. The systems are based on a twodimensional generalization of the notion of sequent, which accounts for a clean formulation of the introduction/elimination rules of the modality. Moreover, the different subsystems are obtained in a modular way, by simple conditions on the elimination rule for !. For the proposed systems we introduce a notion of reduction and we prove a normalization theorem.

1. Introduction

Proof theory of modalities is a delicate subject. The shape of the rules governing the different modalities in the overpopulated world of modal logics is often an example of what a good rule should not be. In the context of sequent calculus, if we want cut elimination, we are often forced to accept rules which are neither left nor right rules, and which completely destroy the deep symmetries the calculus is based upon. In the context of natural deduction the situation is even worse, since we have to admit deduction trees whose subtrees are not deductions, or, in the best case, elimination rules containing in their premise(s) the eliminated connective. On top of this, any such rule do not characterize (in a universal way, as category theoreticians would say) the modality it “defines”: two different modality with the same rules bear no relation among each other (cf. Section 4.1).

As long as modalities are concerned, linear logic is no exception to this situation. Its (exponential) rules are not as bad as that of other modal logics, since they correspond to the modalities of S4, one the most civilized modal logics; still, as the attempt to define a natural deduction system shows (see, e.g., [BBdPH93] for a good discussion of a calculus for the multiplicatives and the exponentials), the rules are asymmetric and do not characterize the modalities. The situation becomes worse if one is interested in subsystems of linear logic where the power of the modalities is, in some way, limited (for instance dropping the property !A ⊸ A and/or the property !A ⊸! !A).

In [Mas92, Mas93] a generalization of the Gentzen format for sequents has been proposed, with the aim of giving a better proof theory for the minimal normal modal logic. The technique, however, is general and applies to a variety of situations where a notion of modality is present. It is the aim of this paper to extend it to some completely linear fragments of intuitionistic multiplicative linear logic, in the sense that we forbid weakening and contraction even on exponential formulas. The resulting systems are weak, but their study seems to provide insight on the fine structure of the exponentials, that is how the several properties they enjoy in the full logic interact.

Cutting down the power of the exponentials, indeed, appears as a promising subject of investigation. Exponentials are the culprits both for undecidability of linear logic and for the hyperexponential complexity of its cut-elimination, and it would be an important result to isolate natural fragments where only one of these “features” appears. An early proposal in this thread is bounded linear logic [GSS92]; an approach similar to our own work is presented in Section 5 of [DJS93] (see also [Sch94, Chap. 7]), where exponentials are indexed over a set equipped with a binary relation.

The main step taken in the natural deduction approach of [Mas93] is a two-dimensional generalization of the notion of sequent. Let us denote formulas with lowercase Greek letters α, β, σ, …, and sequences of formulas with uppercase Greek letters Γ, while ε will be the empty sequence. An intuitionistic 2-sequent is an expression of the form

Authors’ address: Dipartimento di Informatica, Università di Pisa, Corso Italia, 40, I-56125 Pisa, Italy. Email:

{martini,masini}@di.unipi.it.

\begin{matrix}Γ_{1} & & ε \\ Γ_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ Γ_{k} & & σ \end{matrix}  (1)

whose intended meaning is the formula

⋀ Γ_{1} ⊃!(⋀ Γ_{2} ⊃ …!(⋀ Γ_{k} ⊃ σ) …).

Note that the formula σ, the conclusion of the deduction, lies at a level, k, which is greater than, or equal to, the level of any assumption it depends on (any of the Γ_{j}’s may be empty, of course). The propositional rules act over these two dimensional structures in the expected way, just “respecting the levels”. Formulas may change their level only by means of modal rules:

\begin{matrix}Γ_{1} & & ε \\ Γ_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ Γ_{k} & & ε \\ ε & & σ \end{matrix} ; !I ; \begin{matrix}Γ_{1} & & ε \\ Γ_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ Γ_{k} & & !σ \end{matrix}  \begin{matrix}Γ_{1} & & ε \\ Γ_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ Γ_{k} & & !σ \end{matrix} ; !E ; \begin{matrix}Γ_{1} & & ε \\ Γ_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ Γ_{k} & & ε \\ ε & & σ \end{matrix}

Thus, the only way to introduce a modality on a formula occurrence σ at level k is that σ be the only formula present at that level. As a result of the rule, the introduced formula is lifted one level up. Vice versa, the elimination rule pushes a formula down one level (but there is no restriction on its premise). The levels thus represent in the calculus a notion of modal dependence: the conclusion σ at level k modally depends on the assumptions at the same level.

Before going into the details of the systems, we adopt a more compact representation for 2-sequents. Instead of writing two-dimensional judgements, we will denote each formula σ at level k with σ^{k} and write the judgment (1) as Γ ⊢ σ^{k}, where Γ will be seen as a multiset {τ_{1}^{i_{1}}, …, τ_{n}^{i_{n}}}. The reader should always bear in mind, however, that the indexes on formulas are only a metatheoretical notation for two dimensional structures.

2. Completely linear calculi

The standard sequent rules for ! can be divided in two classes: the logical ones (promotion and dereliction), in a sense defining the meaning of the connective; and the structural ones (weakening and contraction), allowing to recover in the context of linear logic the full intuitionistic and classical logic. An important subsystem of linear logic, thus, is the one where we retain the logical !-rules, but we drop the structural ones, giving rise to a “fully linear exponential”. The best way to characterize this system is looking at the properties ! has to satisfy in any model. It is well known (e.g. [Tro91]) that a set of axioms for this purpose is:

\begin{matrix}K & !(α ⊸ β) ⊸ ( !α ⊸!β) \\ T & !α ⊸ α \\ 4 & !α ⊸! !α \end{matrix}

From the point of view of the categorical interpretation of linear logic, K says that ! is a functor, while T and 4 specify, respectively, the two natural transformations, ε and δ, of a comonad.

The level machinery allows a clear and modular study of the several fragments we obtain selecting only some of those axioms. In particular, functoriality of ! will provide the basic introduction/elimination rules, while the natural transformations ε and δ will be obtained by suitable modifications of just the elimination rules. For the systems obtained in this way we will prove normalization.

2.1. Basic definitions

Formulas are built out of atoms (ranged over by p) and the constant 1; compound formulas are obtained with the connectives: ! (unary), ⊗ and ⊸ (binary). Any formula of the calculus will be marked with a level index, varying in ℕ^{+}; an indexed formula σ of level i will be written σ^{i}. A set of assumptions is a set Γ = {σ_{1}^{i_{1}}, …, σ_{n}^{i_{n}}}; for a set of assumptions Γ, define #Γ = max{k_{j} | σ_{j}^{k_{j}} ∈ Γ}; #Γ = 0 when Γ is empty.

Definition 2.1. [Calculus L^{ℓ}] Deductions are inductively defined by the following rules.

σ^{k}

\begin{aligned}& 1I \\ 1^{k} \end{aligned}  \begin{aligned}Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; σ^{k} & & Δ ; \begin{matrix}· \\ · \\ · \end{matrix} ; 1^{j} \\ & & & 1E _{j≤k} \\ & σ^{k} \end{aligned}

\begin{aligned}Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; σ^{k} & Δ ; \begin{matrix}· \\ · \\ · \end{matrix} ; τ^{k} \\ & ⊗I \\ σ ⊗ τ^{k} \end{aligned}  \begin{aligned}Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; σ ⊗ τ^{j} & & [σ^{j}] [τ^{j}] Δ ; \begin{matrix}· \\ · \\ · \end{matrix} ; ρ^{k} \\ & & ⊗E _{j≤k} \\ & ρ^{k} \end{aligned}

Γ [σ^{k}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; τ^{k} ; ⊸ I ; σ ⊸ τ^{k}  \begin{aligned}Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; σ ⊸ τ^{k} & Δ ; \begin{matrix}· \\ · \\ · \end{matrix} ; σ^{k} \\ & & ⊸ E \\ τ^{k} \end{aligned}

where in ⊸ I and ⊗E each discharging is compulsory and involves exactly one formula occurrence.

If S is one of the systems introduced below, we write Γ ⊢_{S} σ^{i} when in S there is a deduction of σ^{i} from the assumptions of the multiset Γ.

2.2. Minimal linear exponential

The first fragment we have in mind is the one where only K is required; the system L^{ℓ}K is obtained from L^{ℓ} by adding the exponential rules:

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; σ^{j} ; !I _{j>#Γ} ; !σ^{j−1}  Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; !σ^{j} ; !E ; σ^{j+1}

We thus have only functoriality of !; axiom K is obtained as follows.

[ !α^{1}] ; !E ; α^{2}  [ !(α ⊸ β)^{1}] ; !E ; α ⊸ β^{2}
⊸ E
β^{2}
!I
!β^{1}
⊸ I
!α ⊸!β^{1}
⊸ I
!(α ⊸ β) ⊸ ( !α ⊸!β)^{1}

Observe that the deduction proceeds exactly as the first order derivation of the formula ∀x(α ⊃ β) ⊃ (∀xα ⊃ ∀xβ).

2.3. T-Linear exponential

Axiom T, that is the comonad natural transformation ε : ! → Id, allows the “elimination” of a ! without incrementing the level index of a formula: ε_{α^{j}} : !α^{j} → α^{j}. The system L^{ℓ}KT is thus obtained extending the !E rule of L^{ℓ}K to take care of this possibility:

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; !σ^{j} ; !E _{k∈\{j, j+1\}} ; σ^{k}

Axiom T can now be proved in a simple way:

[ !α^{1}] ; !E ; α^{1} ; ⊸ I ; !α ⊸ α^{1}

2.4. 4-Linear exponential

Axiom 4, finally, specifies the natural transformation δ : ! →! !. Following the pattern of the previous case, we are thus looking for a rule allowing the derivation

!α^{j} ; \begin{matrix}· \\ · \\ · \end{matrix} ; ! !α^{j}

At this point we could apply twice the minimal rule !E of L^{ℓ}K, obtaining a deduction of α^{j+2} from the assumption !α^{j}. We can pack this deduction in a single rule, and, since we can clearly apply this pattern many times, we can generalize the rule to obtain α^{j+k} from the assumption !α^{j}. The system L^{ℓ}K4 is thus obtained from L^{ℓ}K by extending its !E rule as:

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; !σ^{j} ; !E _{k>j} ; σ^{k}

The crucial fact is that this rule is in fact sufficient to obtain a proof of axiom 4:

[ !α^{1}] ; !E ; α^{3} ; !I ; !α^{2}

!I

! !α^{1}

⊸ I

!α ⊸! !α^{1}

2.5. Full linear exponential

The full power of the linear exponential (axioms K, T, and 4) is recovered in system L^{ℓ}KT 4, whose rule !E encompasses the rules of the same name of the previous systems:

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; !σ^{j} ; !E _{k≥j} ; σ^{k}

Remark. The four systems we have considered, L^{ℓ}K, L^{ℓ}KT, L^{ℓ}K4, and L^{ℓ}KT 4, are distinct, since it can be shown that by relaxing the linearity constraints they respectively yield natural deduction systems for the (positive fragments of the) modal logics K, KT, K4, S4 (after interpreting ! as necessity).

3. Normalization

It remains to show that the proposed calculi can be given a computational interpretation. For each calculus we define, as usual, a correct notion of reduction on deductions, proving the existence of a normalization strategy.

The redexes are defined as expected. In particular, the propositional contractions are standard, since they do not interfere with the level structure. More care has to be taken with the !-rules; in general, a redex is given by the following proof-figure, where the possible values of j depend on the specific calculus.

\begin{matrix}D \\ α^{k} \end{matrix} ; !I ; !α^{k−1} ; !E ; α^{k−1+j}

The level index of the conclusion may be different from the level index of the premise of !I. The same situation arises in the first order calculus, where a redex is:

\begin{matrix}D \\ α \end{matrix} ; !I ; ∀xα ; !E ; [t/x]α

and its reduction requires the substitution of t for x in D. The exact definition of this substitution, though conceptually non deep, is non trivial (see, e.g., [TvD88]). The following definition is for the level indexes what the usual substitution is for terms and variables.

Definition 3.1. [Level substitution] Let D be a deduction of conclusion α^{v}; let i ≥ 2 and n ∈ {−1} ∪ ℕ if v ≥ 2; let i ≥ 1 and n ∈ ℕ if v ≥ 1. We inductively define the deduction [n]_{i}D (read: increment by n any level greater than or equal to i).

If v < i:

[n]_{i} \{ \begin{matrix}D \\ α^{v} \end{matrix} = \begin{matrix}D \\ α^{v} \end{matrix}

If v ≥ i:

• [n]_{i}α^{v} = α^{v+n}

• Let ^{\frac{\begin{matrix}D′ \\ α^{k} \end{matrix} \begin{matrix}D′′ \\ β^{j} \end{matrix}}{γ^{v}}} be a generic rule (possibly unary). Then:

[n]_{i} \{ \underline{\begin{matrix}D′ \\ α^{k} \end{matrix} \begin{matrix}D′′ \\ β^{j} \end{matrix}} ; γ^{v} = \underline{[n]_{i} \{ \begin{matrix}D′ \\ α^{k} \end{matrix} [n]_{i} \{ \begin{matrix}D′′ \\ β^{j} \end{matrix}} ; γ^{v+n}

Observe that the level renaming, in general, affects also the hypotheses of a deduction; the constraint on the application of !I will guarantee that this does not happen during the actual reduction of a redex. One easily proves, moreover, that [0]_{k}D = D. We write [n]_{i}Γ for the application of the level substitution to each formula of Γ.

Before defining the redexes and their contractions, we show that the calculi introduced in the previous section are closed under level substitution.

Lemma 3.2. 1. Let D be a deduction of Γ ⊢_{L^{ℓ}KT} α^{j}, with j ≥ 2. Then, for any 2 ≤ i ≤ j, [−1]_{i}D is a deduction of [−1]_{i}Γ ⊢_{L^{ℓ}KT} α^{j−1}.

2. Let D be a deduction of Γ ⊢_{L^{ℓ}K4} α^{j}, with j ≥ 1. Then, for any 1 ≤ i ≤ j and any k ≥ 1, [k]_{i}D is a deduction of [k]_{i}Γ ⊢_{L^{ℓ}K4} α^{j+k}.

3. Both 1 and 2 hold for deductions in L^{ℓ}KT 4.

Proof. The statements are proved by induction on D. We show the most interesting case of (1); the others are similar and left to the reader. Let D be

Γ ; ⋮ ; !α^{r} ; \overline{α^{j}}

where j = r or j = r + 1. Then,

[−1]_{i}D = [−1]_{i} \{ Γ ; ⋮ ; !α^{r} ; \overline{α^{j−1}}

We have two subcases, depending on the value of i:

1. i ≤ r. By induction hypothesis (note that i ≤ r and 2 ≤ i imply r ≥ 2), we have:

[−1]_{i}D = [−1]_{i}Γ ; ⋮ ; !α^{r−1} ; \overline{α^{j−1}}

2. r < i ≤ j. Then it is the case that j = r + 1; note, moreover, that the indicated level substitution is the identity and that α^{j−1} = α^{r}. The thesis follows by an application of the proper elimination rule of L^{ℓ}KT.

Definition 3.3. [Reduction] We define the redexes and their contractions; the boxed formula is the principal formula of the redex.

• β-contractions:

\begin{aligned}\begin{matrix}[α^{j}] [β^{j}] \\ D \\ γ^{v} \end{matrix} & & \begin{matrix}E′ & E′′ \\ α^{j}  β^{j} \end{matrix} ; ⊗I ; α ⊗ β^{j} \\ & & ⊗E \\ & γ^{v} \end{aligned}  ▷  \begin{matrix}E′ & E′′ \\ α^{j} β^{j} \\ D \\ γ^{v} \end{matrix}

\begin{aligned}\begin{matrix}D′ \\ α^{v} \end{matrix} & \begin{matrix}[α^{v}] \\ D′′ \\ β^{v} \end{matrix} ; ⊸ I ; α ⊸ β^{v} \\ & ⊸ E \\ & β^{v} \end{aligned}  ▷  \begin{matrix}D′ \\ α^{v} \\ D′′ \\ β^{v} \end{matrix}

\begin{matrix}D \\ α^{k} \end{matrix} ; !I ; !α^{k−1} ; !E ; α^{k−1+j}  ▷  \begin{matrix}[j − 1]_{k}D \\ α^{k−1+j} \end{matrix} , where: \{ \begin{matrix}j = 1 & in L^{ℓ}K \\ 0 ≤ j ≤ 1 & in L^{ℓ}KT \\ 1 ≤ j & in L^{ℓ}K4 \\ 0 ≤ j & in L^{ℓ}KT 4 \end{matrix}

• Commutative contractions: With ^{\frac{α^{j}  ⋮}{β^{j+v}}} r we denote a generic rule in \{⊗E, ⊸ E,!E\}, where

α^{j} is the principal premise of the rule r, the vertical dots ⋮ represent some (possible) non principal premise, and β^{j+v} is the conclusion.

\begin{aligned}\begin{matrix}D′ \\ α^{j} \end{matrix}  \begin{matrix}D′′ \\ 1^{k} \end{matrix} ; 1E ; α^{j} & ⋮ \\ & & r \\ β^{j+v} \end{aligned}  ▷  \begin{aligned}\begin{aligned}\begin{matrix}D′ \\ α^{j} \end{matrix} & ⋮ \\ & & r \\ β^{j+v} \end{aligned} & \begin{matrix}D′′ \\ 1^{k} \end{matrix} \\ & & 1E \\ β^{j+v} \end{aligned}

\begin{aligned}\begin{matrix}D′ \\ α ⊗ β^{k} \end{matrix}  \begin{matrix}[α^{k}] [β^{k}] \\ D′′ \\ γ^{j} \end{matrix} ; ⊗E ; γ^{j} & ⋮ \\ & & r \\ δ^{j+v} \end{aligned}  ▷  \begin{aligned}\begin{matrix}D′ \\ α ⊗ β^{k} \end{matrix} & & \begin{aligned}\begin{matrix}[α^{k}] [β^{k}] \\ D′′ \\ γ^{j} \end{matrix} & ⋮ \\ & & r \\ δ^{j+v} \end{aligned} \\ & & ⊗E \\ & δ^{j+v} \end{aligned}

The degree of a redex is the structural complexity of its principal formula.

We need to show that the different systems are stable under normalization.

Proposition 3.4. Let S be a system in {L^{ℓ}K, L^{ℓ}KT, L^{ℓ}K4, L^{ℓ}KT 4}. The contractions of Definition 3.3 are correct for S.

Proof. Correctness of propositional and commutative contractions is obvious; we thus take into account only !-contraction. If the LHS of the !-contraction is a deduction in S establishing Γ ⊢_{S} α^{k−1+j}, then, by Lemma 3.2, the contractum is still a deduction in S, establishing [j−1]_{k}Γ ⊢_{S} α^{k−1+j}. But the side condition on the application of !I ensures that k is greater than the level of any formula in Γ, namely [j − 1]_{k}Γ = Γ.

The compatible closure of ▷ (or one-step reduction) is denoted with →; its transitive closure is →^{+}, while ↠ (the reduction relation) is the transitive and reflexive closure.

Theorem 3.5. Let D be a deduction of Γ ⊢_{L^{ℓ}KT 4} and let D ↠ D′. Then also D′ is a deduction of Γ ⊢_{L^{ℓ}KT 4}.

Proof. By induction on the length of the reduction, using Proposition 3.4.

Theorem 3.6 (Normalization) The ↠ relation is normalizing.

Proof. (Sketch: For a detailed discussion of the standard intuitionistic case, which is technically the same, see [TvD88, 530–537].) Define the degree, d(D), of a deduction D as the maximum of the degrees of the redexes in D. Set now μ(D) = (d(D), m), where m is the sum of the lengths of the maximal redexes (i.e. redexes of degree d(D)) in D. By induction on μ(D) (under the lexicographic ordering) we prove that, selected a redex of maximal degree in D, we can reduce μ(D).

4. Discussion

4.1. On the universality of !

It is well known that usual presentations of modal logics (both in sequent calculi and in natural deduction systems) do no allow to prove the equivalence of two modalities enjoying exactly the same rules. Standard presentations of linear logic have the same defect; for example it is possible to add to linear logic another exponential, say ¡, with exactly the same rules of !, but it is impossible to prove that ⊢!α ∘−∘ ¡α. In fact, the introduction of a ! is constrained not by structural properties of proofs (or in the case of sequent formulations, by structural properties of sequents), but by the syntactical shape of the premises. At a first level, our formulation has not this kind of problems, as the following proposition shows.

Proposition 4.1. Let S be one of the linear logic systems previously defined. Let us duplicate the exponential rules of S with a new exponential ¡, and call S¡ the resulting system. Then

⊢_{S¡} !α∘−∘¡α^{j}

for each level j.

Proof. Let us prove that ¡α ⊸!α^{j}.

[¡α^{j}] ; ¡E ; α^{j+1} ; !I ; !α^{j}

⊸ I

¡α ⊸!α^{j} This happens because ! and ¡ share the same level structure; if we added another level structure, different from the first, and we defined ¡ in terms of the new levels, then the anomaly would be there again.

4.2. Linear lambda-calculi

The choice of a natural deduction presentation allows a simple computational interpretation of the proposed fragments of linear logic. It is straightforward to decorate the deductions with λ-terms. A suitable syntax for the modal rules and their contraction is the following:

\begin{matrix}D \\ M : α^{k} \end{matrix} ; !I ; gen(M)^{k−1} : !α^{k−1} !E ungen(gen(M)^{k−1})^{k−1+j} : α^{k−1+j} ▷ \begin{matrix}[j − 1]_{k}D \\ [j − 1]_{k}M : α^{k−1+j} \end{matrix}

As an example, the following are the terms representing the given proofs for the three exponential axioms K, T and 4.

λy^{1}.λx^{1}.gen((ungen(y^{1})^{2}ungen(x^{1})^{2})^{2})^{1} : □(α ⊃ β) ⊃ (□α ⊃ □β)^{1}

(λx^{1}.ungen(x^{1})^{1})^{1} : □α ⊃ α^{1}

(λx^{1}.gen(gen(ungen(x^{1})^{3})^{2})^{1})^{1} : □α ⊃ □□α^{1}

4.3. Relations with proof-nets

An anonymous referee suggested an interesting interpretation of our work in terms of proof-nets, as proposed in [Reg92]. For the purpose of this discussion, we may assume such nets as composed of links of two kinds, ? and !; each time a link ! is added to a net, also a box is given, whose ports different from the ! link are all ? links. It should be clear that the creation of a !-link corresponds to !-introduction, while the creation of ?-links corresponds to !-elimination.

On these nets we may investigate the lift of a ?-link, that is the number of boxes the link may cross; setting suitable constraints on the allowed lifts results in constraining !-elimination. The lift of a ?-link exactly corresponds, in our approach, to the difference between the level of the conclusion and the level of the premise in the !-elimination rule. Thus, if we only allow lifts of 1, we obtain L^{ℓ}K; lifts in {0, 1} yield L^{ℓ}KT, lifts in {p | p ≥ 1} yield L^{ℓ}K4, while unrestricted lifts gives full linear exponentials. It is not too difficult to check that these four sets of allowed lifts are all stable under proof-net reduction, a result matching our Lemma 3.2. As a corollary, one obtains immediately strong normalization and confluence for the proposed systems.

More systems enjoy the same properties. For L ⊆ ℕ (the set of allowed lifts), let L^{ℓ}L be the system with lifts only in L (thus L^{ℓ}KT is L^{ℓ}{0, 1}, etc.); it can be shown that L^{ℓ}L is closed under reduction iff L = {0} or {i + j − 1 | i, j ∈ L ∧ j ≠ 0} ⊆ L. In terms of levels, this results in the following generalization of Lemma 3.2.

Proposition 4.2. Let D be a deduction of Γ ⊢_{L^{ℓ}L} α^{j}.

1. If 0 ∈ L, then for any 2 ≤ i ≤ j, [−1]_{i}D is a deduction of [−1]_{i}Γ ⊢_{L^{ℓ}L} α^{j−1}.

2. For any p ∈ L, p ≠ 0, and any 1 ≤ i ≤ j, [p − 1]_{i}D is a deduction of [p − 1]_{i}Γ ⊢_{L^{ℓ}L} α^{j+p−1}.

We thus have infinitely many fragments (e.g. L may be the set of odd numbers), all closed under reduction and enjoying strong normalization and confluence, although none of them seems to bear a real interest (the “characteristic formulas” of L^{ℓ}L are !A ⊸!^{p}A, for p ∈ L).

Acknowledgments

Section 4.3 is essentially due to an anonymous referee, which we sincerely thank.

References

[BBdPH93] N. Benton, G. Bierman, V. de Paiva, and J.M.E. Hyland. Linear λ-calculus and categorical models revisited. In E. Börger et al., editors, Computer Science Logic 1992, volume 702 of Lectures Notes in Computer Science, pages 61–84. Springer-Verlag, 1993.

[DJS93] V. Danos, J.-B. Joinet, and H. Schellinx. The structure of exponentials: uncovering the dynamics of linear logic proofs. In G. Gottlob et al., editors, Computational Logic and Proof Theory, volume 713 of Lecture Notes in Computer Science, pages 159–171. Springer-Verlag, 1993. Proc. of Third Kurt Gödel Colloquium, Brno, August 1993.

[GSS92] J.-Y. Girard, A. Scedrov, and P.J. Scott. Bounded linear logic: A modular approach to polynomial time computability. Theoretical Computer Science, 97:1–66, 1992.

[Mas92] Andrea Masini. 2-sequent calculus: A proof theory of modalities. Annals of Pure and Applied Logic, 58:229–246, 1992.

[Mas93] Andrea Masini. 2-sequent calculus: Intuitionism and natural deduction. Journal of Logic and Computation, 3:1–31, 1993.

[Reg92] Laurent Regnier. Lambda-Calcul et Réseaux. Thèse de doctorat, Université Paris 7, 1992.

[Sch94] H. Schellinx. The Noble Art of Linear Decorating. ILLC dissertation series 1994-1, Institute for Logic, Language and Computation, Universiteit Amsterdam, 1994.

[Tro91] Anne Troelstra. Lectures on Linear Logic. CSLI Lecture Notes. Chicago University Press, 1991.

[TvD88] Anne Troelstra and Dirk van Dalen. Constructivism in Mathematics, volume II. North-Holland, 1988.