Coherence for Frobenius pseudomonoids and the geometry of linear proofs

TL;DR

This paper establishes coherence theorems for Frobenius pseudomonoids, leading to a 3D proof notation for linear logic that simplifies proof equivalence without global correctness criteria.

Contribution

It introduces a 3D diagrammatic framework for linear logic proofs based on coherence theorems, connecting categorical structures with proof representations.

Findings

Provides a 3D notation for linear logic proofs

Eliminates need for global correctness criteria in proof verification

Shows traditional proof nets as 2D projections of 3D diagrams

Abstract

We prove coherence theorems for Frobenius pseudomonoids and snakeorators in monoidal bicategories. As a consequence we obtain a 3d notation for proofs in nonsymmetric multiplicative linear logic, with a geometrical notion of equivalence, and without the need for a global correctness criterion or thinning links. We argue that traditional proof nets are the 2d projections of these 3d diagrams.