A uniform cut-elimination theorem for linear logics with fixed points and super exponentials

TL;DR

This paper introduces a unified cut-elimination theorem for a broad class of linear logics with fixed points and super exponentials, simplifying proof theory across multiple systems.

Contribution

It provides a uniform cut-elimination theorem for parametrized systems with fixed-points, combining reduction-based proofs and sufficient condition identification.

Findings

Unified cut-elimination theorem for various linear logics

Applicable to systems inspired by subexponentials and super exponentials

Bridges proof theory of light logics with recursive types and modal μ-calculus.

Abstract

In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induces the need for cut-elimination theorems for each logic, the proof of which may be redundant. A number of approaches in proof theory have been adopted to cope with this need. In the present paper, we consider this issue from the point of view of enhancing linear logic with least and greatest fixed-points and considering such a variety of exponential connectives. Our main contribution is to provide a uniform cut-elimination theorem for a parametrized system with fixed-points by combining two approaches: cut-elimination proofs by reduction (or translation) to another system and the identification of sufficient conditions for cut-elimination. More precisely, we examine a broad range of systems, taking inspiration from Nigam and Miller's subexponentials and from Bauer and Laurent's super exponentials. Our work is motivated on the one hand by Baillot's work on light logics with recursive types and on the other hand by Bauer and Saurin's recent work on the proof theory of the modal {\mu}-calculus.