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 two-dimensional 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.

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).