Proof Nets

Origin. Girard (1987) for linear logic. Graph representation of proofs. Identifies proofs differing only by inessential rule permutations. Correctness criterion replaces derivation trees.

Models. Proofs as graphs with typed links. Links for each connective. Correctness: no vicious cycles. Cut elimination as graph rewriting. Canonical proof representation.

Formalism.

Links: Axiom link: connects dual atoms A, A⊥ Cut link: connects A, A⊥ for elimination ⊗-link: binary, two premises, one conclusion (A⊗B) ⅋-link: binary, two premises, one conclusion (A⅋B) !-link: box structure for exponentials

Both multiplicative links have the same shape — two premises, one conclusion. Arity is not what separates them, and it cannot be: the Danos–Regnier switching below chooses one premise of each ⅋, which is only meaningful if ⅋ has two. What separates them is that a ⊗-link splits the net into two disjoint subnets while a ⅋-link does not, and the switching is precisely the test for that.

Multiplicative proof net: Graph satisfying:

Each formula occurrence connected once
Correctness criterion (Danos-Regnier)

Correctness criterion: DR-switching: choose one premise for each ⅋. Correct iff all switchings give connected acyclic graphs.

Cut elimination: Axiom-cut: remove both links. ⊗-⅋: rewire connections. !-?: box reduction rules. Strongly normalizing.

MLL proof nets: A A⊥ \ / ax Axiom link

A B \ / ⊗ Tensor link | A⊗B

A B \ / ⅋ Par link — same shape, two premises | A⅋B

Exponential boxes: !-box: bounded subgraph. Contraction, weakening, dereliction at box boundary.

Symbols.

Symbol	Unicode	Name	Meaning
⊗	U+2297	Tensor	Multiplicative conjunction; its link splits the net
⅋	U+214B	Par	Multiplicative disjunction; its link is the one switched
⊥	U+22A5	Up tack / Linear negation	Written postfix: A⊥ is the dual of A
!	U+0021	Exclamation mark / Of course	Exponential; its link is a box
?	U+003F	Question mark / Why not	Dual exponential; contraction and weakening at the box border
ax	—	Axiom link	Connects an atom to its dual
cut	—	Cut link	Connects A to A⊥ for elimination
DR	—	Danos–Regnier	The switching correctness criterion
MLL	—	Multiplicative linear logic	The fragment in which nets are best behaved

Metatheory. Girard (1987) introduced proof nets so that sequent derivations differing only by permutations of independent rules would be one object, and for unit-free MLL the quotient is exact: nets are canonical representatives of proofs modulo rule permutation. The Danos–Regnier criterion (1989) says which proof structures are nets — every switching, got by selecting one premise of each ⅋, must be acyclic and connected — and although the naive test inspects 2ⁿ switchings for n par-links, correctness is decidable in linear time (Guerrini; Murawski and Ong). Cut elimination is local graph rewriting, strongly normalizing and confluent, and unlike its sequent counterpart it is parallel, since independent redexes reduce independently. The complexity is nonetheless high: provability in MLL is NP-complete (Kanovich), Lincoln, Mitchell, Scedrov and Shankar (1992) proved full propositional linear logic undecidable, and decidability of MELL remains open.

Applies to. Linear logic. Parallel proof reduction. Proof semantics. Implicit complexity. Certified proof checkers.

Limitations. Canonicity is confined to a fragment. Adding the multiplicative units destroys it: Heijltjes and Houston (2014) proved that deciding equivalence of MLL proofs with units is PSPACE-complete, so nets in the unit-free sense cannot be extended to the units. Exponentials are handled by boxes, which reintroduce exactly the sequential bracketing nets were meant to remove — a box is a subgraph delimited as a unit, so exponential nets are not fully parallel and the quotient by rule permutation is only partial. Additives needed a different device altogether: Hughes and van Glabbeek (2005) built unit-free MALL nets from slicings, not from an extension of the multiplicative links. Correctness checking for nets with boxes has no known linear algorithm, and every non-commutative variant requires its own criterion.