Logic in Computer Science, 2018

Proof nets for MLL (unit-free Multiplicative Linear Logic) are concise graphical
representations of proofs which are *canonical* in the sense that they abstract away
syntactic redundancy such as the order of non-interacting rules. We argue that
Girard’s extension to MLL1 (first-order MLL) fails to be canonical because of
redundant existential witnesses, and present canonical MLL1 proof nets called
*unification nets* without them. For example, while there are infinitely many
cut-free Girard nets ∀x Px ⊢ ∃x Px, one per arbitrary witness for ∃x,
there is a unique cut-free unification net, with no specified witness.

Cut elimination for unification nets is local and linear time, while Girard’s is non-local and exponential time. Since some unification nets are exponentially smaller than corresponding Girard nets and sequent proofs, technical delicacy is required to ensure correctness is polynomial-time (quadratic).

These results transcend MLL1 via a methodological insight: for
canonical quantifiers, the standard *parallel/sequential*
dichotomy of proof nets is insufficient; an *implicit/explicit*
witness dichotomy is needed. Current work extends unification
nets to additives and uses them to extend *combinatorial proofs* [Proofs
without syntax, Annals of Mathematics, 2006] to classical first-order
logic.