Cut Elimination in Multifocused Linear Logic

TL;DR

This paper investigates cut elimination procedures in a multifocused version of linear logic, addressing unique challenges posed by the multifocusing phases and establishing a method to perform cut elimination effectively.

Contribution

It introduces a novel approach to cut elimination in multifocused linear logic, handling complexities from multifocusing phases not present in standard focused systems.

Findings

Cut elimination is feasible in multifocused linear logic.

Multifocusing phases introduce unique challenges in proof normalization.

Specific lemmas are necessary to manage multifocusing during cut elimination.

Abstract

We study cut elimination for a multifocused variant of full linear logic in the sequent calculus. The multifocused normal form of proofs yields problems that do not appear in a standard focused system, related to the constraints in grouping rule instances in focusing phases. We show that cut elimination can be performed in a sensible way even though the proof requires some specific lemmas to deal with multifocusing phases, and discuss the difficulties arising with cut elimination when considering normal forms of proofs in linear logic.