On the fine structure of the exponential rule

The authors investigate fragments of intuitionistic linear logic with the connectives ⊗, →, ! and the constant 1, in which weakening and contraction is not allowed even on modalized formulas. Instead, some rules are retained corresponding to the axioms (K) !(A→B)→(!A→!B), (T) !A→A, and (4) !A→!!A. The formulation in natural deduction style is obtained via the so-called 2-sequent calculus of Masini [Ann. Pure Appl. Logic 58 (1992), no. 3, 229--246; MR1191942 (93k:03056)]. Thus formulas in deductions are indexed by positive integers ("levels''), and the propositional rules preserve the levels; the introduction rule for ! is Aj/!Aj−1 provided j is bigger than any level of any formula occurring in open assumptions. The elimination rule depends on the fragment chosen; for the full KT4 fragment it is !Aj/Ak (k≥j). Via a careful definition of reductions on derivations (which in the exponential case also requires a suitable rewriting of the levels in the contractum) the authors prove a normalization result. By comparison with proof-nets it is maintained, without proof, that strong normalization and confluence hold for the given reduction relation.