# Linear logic with contraction

What is the proof system obtained when adding a contraction rule to linear logic or removing the weakening rule from intuitionistic logic? In other words, what goes in the missing cell of the following table?

No contraction Contraction
No weakening Linear logic ?
Weakening Affine logic Intuitionistic logic

Intuitively, this will mean that one has to list all hypotheses, and no more are used to prove a given result, but it doesn't matter how many times each hypothesis is used.

The name of such a system and a few links would be enough.

• Commented May 23 at 9:38
• I guess you know that addition of structural rules "contraction" and "weakening" can have drastic side effects on (multiplicative) linear logic. I think this is mentioned in Girard's original article on Linear Logic, and it's certainly mentioned in his Proofs and Types. From a semantic point of view, thinking of star-autonomous categories as modeling MLL, the addition of these structural rules restricts the models right back down to Boolean algebras or Boolean preorders, as shown by Joyal. Commented May 24 at 12:45

Note that there is not only one relevant logic but a pletora of relevant logics, such as system $$R$$ and its variants (see here for a proof-theoretical study of one of these variants), and they may differ from each other in a very considerable way. In general, all these systems are not simply obtained from intuitionistic logic by dropping the weakening rule, since otherwise there would be unpleasant consequences such as the lack of distributivity of conjunction over disjunction (see here). As a consequence, the study of their proof systems and the techinicalities used for that may be quite sophisticated (or awkward, depending on the point of view).