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, one premise, two conclusions !-link: box structure for exponentials

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

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.