In
proof theory
Proof theory is a major branchAccording to , proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. consists of four corresponding parts, with part D being about "Proof The ...
, proof nets are a geometrical method of representing proofs that
eliminates two forms of ''bureaucracy'' that differentiate proofs: (A) irrelevant syntactical features of regular proof calculi, 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. This distinguishes proof nets from regular proof calculi such as the
natural deduction
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use ...
calculus and the
sequent calculus
In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautolog ...
, where these phenomena are present. Proof nets were introduced by
Jean-Yves Girard
Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is a research director (emeritus) at the mathematical institute of University of Aix-Marseille, at Luminy.
Biography
Jean-Yves Girard is an alumnus of the Éc ...
.
As an illustration, these two
linear logic
Linear logic is a substructural logic proposed by French logician Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the ...
proofs are identical:
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,
[Girard, Jean-Yves. ]
Linear logic
', Theoretical Computer Science
Theoretical computer science is a subfield of computer science and mathematics that focuses on the Abstraction, abstract and mathematical foundations of computation.
It is difficult to circumscribe the theoretical areas precisely. The Associati ...
, Vol 50, no 1, pp. 1–102, 1987 which was described by
Jean-Yves Girard
Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is a research director (emeritus) at the mathematical institute of University of Aix-Marseille, at Luminy.
Biography
Jean-Yves Girard is an alumnus of the Éc ...
.
See also
*
Linear logic
Linear logic is a substructural logic proposed by French logician Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the ...
*
Ludics
*
Geometry of interaction
*
Coherent space
*
Deep inference
*
Interaction nets
References
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
Proof theory
{{logic-stub