EXPERIMENTS IN LINEAR NATURAL DEDUCTION

We investigate several fragments of multiplicative linear logic, in a natural deduction setting and with the aim of a better understanding o f the par connective. We study, first, a pre-tensorial calculus, which is strengthened then in the standard tensorial fragment. The addition of a further pre-tensorial connective yields (a natural deduction ver sion of) Full Intuitionistic Linear Logic. A further strengthening of the rules leads to the full classical multiplicative logic. Some proof -theoretical properties of the systems are investigated.