  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 $\forall x Px \vdash \exists xPx$, one
per arbitrary choice of witness for $\exists x$, there is a unique cut-free
unification net, with no specified witness.
  Redundant existential witnesses cause Girard's MLL1 nets to suffer from
severe complexity issues: (1) cut elimination is non-local and exponential-time
(and -space), and (2) some sequents require exponentially large cut-free Girard
nets. Unification nets solve both problems: (1) cut elimination is local and
linear-time, and (2) cut-free unification nets grow linearly with the size of
the sequent. 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 extend beyond MLL1 via a broader methodological insight: for
canonical quantifiers, the standard parallel/sequential dichotomy of proof nets
fails; an implicit/explicit witness dichotomy is also needed. Work in progress
extends unification nets to additives and uses them to extend combinatorial
proofs [Proofs without syntax, Annals of Mathematics, 2006] to classical
first-order logic.
