Exponentially Handsome Proof Nets and Their Normalization

TL;DR

This paper extends handsome proof nets to include units and exponentials in multiplicative linear logic, introduces a new sequent system, and develops normalization procedures for these graphical proofs.

Contribution

It introduces exponentially handsome proof nets with cuts, a new sequent system, and a normalization process, advancing the graphical proof theory for linear logic.

Findings

Sound and complete sequent system for extended logic

Graphical proof system capturing proof equivalence

Normalization procedure for exponential proof nets

Abstract

Handsome proof nets were introduced by Retor\'e as a syntax for multiplicative linear logic. These proof nets are defined by means of cographs (graphs representing formulas) equipped with a vertices partition satisfying simple topological conditions. In this paper we extend this syntax to multiplicative linear logic with units and exponentials. For this purpose we develop a new sound and complete sequent system for the logic, enforcing a stronger notion of proof equivalence with respect to the one usually considered in the literature. We then define combinatorial proofs, a graphical proof system able to capture syntactically the proof equivalence, for the cut-free fragment of the calculus. We conclude the paper by defining the exponentially handsome proof nets as combinatorial proofs with cuts and defining an internal normalization procedure for this syntax.