User:JLLong/Proof net

In proof theory and linear logic, proof nets are graphical proofs which eliminate inessential details needed in more traditional forms of proof (especially sequent proofs). A proof net is both a verifiable witness to the provability of a logical formula and a geometric object subject to dynamical rules (cut-elimination). In linear logic, proof nets play a role analogous to that of natural deduction in intuitionistic logic, but with greater economy afforded by linear duality.

Proof nets trade the elimination of inessential details for a more complex, nonlocal notion of correctness. Sequent proofs are locally verifiable: a proof is valid so long as each step follows the rules of sequent calculus. On the other hand, proof net correctness is subtle and nonlocal. Graphs which follow the local rules for constructing proof nets (but need not actually represent proofs) are called proof structures.

Every sequent proof gives rise to one proof net, but one proof net may correspond to many sequent proofs.

Proof nets are not a single formal specification, but rather an idea applied to several logic systems, especially linear logic and its fragments and variations. Of these, the proof nets for multiplicative linear logic are considered indisputable, while those for other fragments are the subject of research.

History

Proof nets for multiplicative linear logic

Proof nets were introduced by Jean-Yves Girard along with linear logic in 1987. At that time, Girard gave a satisfactory notion of proof net for the multiplicative fragment (which has remained unchanged since), and included other fragments through mechanisms he considered unsatisfactory. Girard's algorithm for correctness (the "long-trip criterion") is exponential-time.

In his PhD thesis (year?), Vincent Danos formulated multiplicative proof net correctness through graph transformation rules known as contractibility. Danos and Regnier simplified Girard's long-trip criterion, making correctness equivalent to certain subgraphs being trees.

In 1994 Guerrini as well and Dominic and Ong gave linear-time algorithms for multiplicative proof net correctness. Since correctness has a trivial linear lower bound, this is asymptotically optimal.

Other fragments and variants

Proof nets have been formulated for additive linear logic, multiplicative-exponential linear logic, multiplicative-additive linear logic (cite monomial, hughes), and versions of non-commutative logic.

Including units (examples) in proof nets is nontrivial, though various proposal exist.

Multiplicative proof nets

As an illustration, these two linear logic proofs are 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 (i.e. something that seems to be a proof net) is actually a concrete proof structure (i.e. something that 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
• Interaction nets

Sources

• Proofs and Types. Girard J-Y, Lafont Y, and Taylor P. Cambridge Press, 1989.
• Roberto Di Cosmo and Vincent Danos, The Linear Logic Primer
• Sean A. Fulop, A survey of proof nets and matrices for substructural logics