Isomorphism

From LLWiki
(Difference between revisions)
Jump to: navigation, search
m (notation for isomorphisms)
(Link to list of isomorphisms)
 
Line 17: Line 17:
 
<math>\LabelRule{\rulename{ax}}\NulRule{A\vdash A}\DisplayProof</math>.
 
<math>\LabelRule{\rulename{ax}}\NulRule{A\vdash A}\DisplayProof</math>.
   
Some well known isomorphisms of linear logic are the following ones:
+
Linear logic admits [[List of isomorphisms|many isomorphisms]], but it is not known wether all of them have been discovered or not.
* <math>A\tens B \limp C \cong A\limp B \limp C</math>
 
* …
 

Latest revision as of 20:38, 25 April 2013

This page is a stub and needs more content.


Two formulas A and B are isomorphic (denoted A\cong B), when there are two proofs π of A \vdash B and ρ of B \vdash A such that eliminating the cut on A in

\AxRule{}\VdotsRule{\pi}{A \vdash B}\AxRule{}\VdotsRule{\rho}{B \vdash A}\LabelRule{\rulename{cut}}\BinRule{B\vdash B}\DisplayProof

leads to an η-expansion of

\LabelRule{\rulename{ax}}\NulRule{B\vdash B}\DisplayProof,

and eliminating the cut on B in

\AxRule{}\VdotsRule{\pi}{A \vdash B}\AxRule{}\VdotsRule{\rho}{B \vdash A}\LabelRule{\rulename{cut}}\BinRule{A\vdash A}\DisplayProof

leads to an η-expansion of

\LabelRule{\rulename{ax}}\NulRule{A\vdash A}\DisplayProof.

Linear logic admits many isomorphisms, but it is not known wether all of them have been discovered or not.

Personal tools