Proof net
Encyclopedia
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:
And their corresponding nets will be the same.
.
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, 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
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...
calculus and the sequent calculus
Sequent calculus
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
, 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
Jean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
.
For instance, these two linear logic
Linear logic
Linear logic is a substructural logic proposed by 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...
proofs are “morally” identical:
|
|
|
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 GirardJean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
.
See also
- Linear logicLinear logicLinear logic is a substructural logic proposed by 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...
- LudicsLudicsIn proof theory, ludics is an analysis of the principles governing inference rules of mathematical logic. Key features of ludics are its notion of compound connectives using a technique known as focusing or focalisation , and its use of locations or loci over a base instead of propositions.More...
- Geometry of interactionGeometry of interactionThe geometry of interaction was introduced by Jean-Yves Girard shortly after his work on Linear Logic. In linear logic, proofs can be seen as some kind of networks instead of the flat tree structure of sequent calculus. To distinguish the real proof nets from all the possible networks, Girard...
- Coherent spaceCoherent spaceIn proof theory, a coherent space is a concept introduced in the semantic study of linear logic.Let a set C be given. Two subsets S,T ⊆ C are said to be orthogonal, written S ⊥ T, if S ∩ T is ∅ or a singleton...
- Deep inferenceDeep inferenceDeep inference names a general idea in structural proof theory that breaks with the classical sequent calculus by generalising the notion of structure to permit inference to occur in contexts of high structural complexity...
- Interaction netsInteraction netsInteraction nets are a low level graphical computation paradigm first proposed by Yves Lafont and based on Jean-Yves Girard's proof nets for linear logic...