Isomorphism
From LLWiki
(Difference between revisions)
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 21:38, 25 April 2013
This page is a stub and needs more content.
Two formulas A and B are isomorphic (denoted 
), when there are two proofs π of 
and ρ of 
such that eliminating the cut on A in
leads to an η-expansion of
,
and eliminating the cut on B in
leads to an η-expansion of
.
Linear logic admits many isomorphisms, but it is not known wether all of them have been discovered or not.
