From Proof Nets to the Free *-Autonomous Category

TL;DR

This paper develops a comprehensive theory of proof nets for full multiplicative linear logic, including units, and demonstrates that these nets form the free *-autonomous category, extending existing frameworks.

Contribution

It introduces a new tree-based linking structure for proof nets with units and proves their correspondence to the free *-autonomous category.

Findings

Proof nets with tree-based links are equivalent under graph rewriting.

Sequentialization and normalization results are established.

Proof nets characterize the free *-autonomous category.

Abstract

In the first part of this paper we present a theory of proof nets for full multiplicative linear logic, including the two units. It naturally extends the well-known theory of unit-free multiplicative proof nets. A linking is no longer a set of axiom links but a tree in which the axiom links are subtrees. These trees will be identified according to an equivalence relation based on a simple form of graph rewriting. We show the standard results of sequentialization and strong normalization of cut elimination. In the second part of the paper we show that the identifications enforced on proofs are such that the class of two-conclusion proof nets defines the free *-autonomous category.