MALL proof nets identify proofs modulo rule commutation

TL;DR

This paper proves that MALL proof nets precisely identify cut-free proofs up to rule commutation, extending to include the mix rule and cut, clarifying the structure of proofs in linear logic.

Contribution

It establishes a complete correspondence between proof nets and proofs modulo rule commutation for MALL, including the mix rule and cut, enhancing understanding of proof equivalences.

Findings

Proof nets identify proofs modulo rule commutation in MALL

The result holds with and without the mix rule

Extension of the result to include cut proofs

Abstract

We show that the proof nets introduced in [Hughes & van Glabbeek 2003, 2005] for MALL (Multiplicative Additive Linear Logic, without units) identify cut-free proofs modulo rule commutation: two cut-free proofs translate to the same proof net if and only if one can be obtained from the other by a succession of rule commutations. This result holds with and without the mix rule, and we extend it with cut.