Multiplicative Exponential Linear Logic

Multiplicative Exponential Linear Logic (MELL) is the fragment of linear logic consisting of

• the multiplicative connectives \otimes and ⅋
• the exponential modalities ! and ?
• (optionally) their multiplicative units \mathbf{1} and \bot

Because of the presence of ⅋, MELL is a fragment of classical linear logic. A similar fragment without ⅋ is usually referred to as Intuitionistic Linear Logic.

Proof nets

Please expand.

Models

Please expand.

Decidability

Please expand.

See also

• Linear Logic
• Multiplicative Linear Logic