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
ax	—	Axiom	Identity link
cut	—	Cut	Elimination
⊗	U+2297	Tensor	Multiplicative and
⅋	U+214B	Par	Multiplicative or
!	—	Box	Exponential

Metatheory. Proof identity: nets modulo link ordering. Strong normalization. Confluence. Denotational semantics in coherence spaces. Geometry of interaction.

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

Limitations. Exponentials require boxes (complex). Non-commutative variants harder. Correctness checking can be expensive. MLL tractable, full LL harder.