Cut Elimination in Multifocused Linear Logic

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