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 20: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.