Proof net

In proof theory, proof nets are a geometrical method of representing proofs that eliminates two forms of bureaucracy that differentiates proofs: (A) irrelevant syntactical features of regular proof calculi such as the natural deduction calculus and the sequent calculus, and (B) the order of rules applied in a derivation. In this way, the formal properties of proof identity correspond more closely to the intuitively desirable properties. Proof nets were introduced by Jean-Yves Girard.

For instance, these two linear logic proofs are “morally” identical:

$\vdash$ A, B, C, D $\vdash$ A ⅋ B, C, D $\vdash$ A ⅋ B, C ⅋ D

$\vdash$ A, B, C, D $\vdash$ A, B, C ⅋ D $\vdash$ A ⅋ B, C ⅋ D

And their corresponding nets will be the same.

Correctness criteria

Several correctness criteria are known to check if a sequential proof structure (ie. something which seems to be a proof net) is actually a concrete proof structure (ie. something which encodes a valid derivation in linear logic). The first such criterion is the long-trip criterion which was described by Jean-Yves Girard.

See also

• Linear logic
• Ludics
• Geometry of interaction
• Coherent space
• Deep inference
• Interaction nets

References

• Proofs and Types. Girard J-Y, Lafont Y, and Taylor P. Cambridge Press, 1989. (An electronic version is online at [1].)
• Roberto Di Cosmo and Vincent Danos, The Linear Logic Primer [2]