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 of 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 version 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.

Authors

• Simone Martini
• Andrea Masini

Keywords

No keywords are indexed for this paper.