Super Exponentials in Linear Logic

TL;DR

This paper introduces Superexponential Linear Logic (superLL), a parameterized system that generalizes various existing linear logic variants and proves cut elimination under certain conditions.

Contribution

It proposes superLL, a new flexible framework that unifies multiple linear logic systems and establishes cut elimination for its variants.

Findings

Superexponential Linear Logic (superLL) generalizes existing systems like ELL, LLL, and SLL.

A generic proof of cut elimination is provided for superLL under specific constraints.

All instances of superLL satisfy cut elimination, ensuring consistency and normalization.

Abstract

Following the idea of Subexponential Linear Logic and Stratified Bounded Linear Logic, we propose a new parameterized version of Linear Logic which subsumes other systems like ELL, LLL or SLL, by including variants of the exponential rules. We call this system Superexponential Linear Logic (superLL). Assuming some appropriate constraints on the parameters of superLL, we give a generic proof of cut elimination. This implies that each variant of Linear Logic which appears as a valid instance of superLL also satisfies cut elimination.