Systems of Natural Deduction for Intuitionistic Linear Logic

Sara Negri

We present a system of natural deduction with implicit structural rules for intuitionistic linear logic. Each connective as well as the modality ! has an introduction and an elimination rule. No explicit weakening or contraction rules for !-formulas are needed. These structural rules are absorbed into a generalized form of the rule of introduction for the ! modality.

General elimination rules were introduced in von Plato (1998) and systematically employed in Negri and von Plato (2001) in order to obtain a close correspondence between natural deduction and sequent calculus and between normalization and cut-elimination for intuitionistic and classical logic.

Here the method is extended to intuitionistic linear logic by employing general elimination rules for all connectives and quantifiers, and also for the !-modality. Normalization thus follows through translation to sequent calculus and cut-elimination. The subformula property obtains for all normal derivations with instances of the rule of !-introduction of a prescribed form. A second system with explicit structural rules has the full subformula property for normal derivations. Other methods of absorbing the structural rules into rules that discharge assumptions are presented.

Negri, S. and J. von Plato (2001) Structural Proof Theory, Cambridge University Press, in press.

von Plato, J. (1998) Natural deduction with general elimination rules, submitted.

Address: Department of Philosophy, PL 24, Unioninkatu 40 B, 00014 University of Helsinki, Finland

E-mail: negri@helsinki.fi