Isomorphism
From LLWiki
(Difference between revisions)
Lionel Vaux (Talk | contribs) m (added template stub) |
m (notation for isomorphisms) |
||
| Line 1: | Line 1: | ||
{{stub}} |
{{stub}} |
||
| − | Two formulas <math>A</math> and <math>B</math> are isomorphic, when there are two proofs <math>\pi</math> of <math>A \vdash B</math> and <math>\rho</math> of <math>B \vdash A</math> such that eliminating the cut on <math>A</math> in |
+ | Two formulas <math>A</math> and <math>B</math> are isomorphic (denoted <math>A\cong B</math>), when there are two proofs <math>\pi</math> of <math>A \vdash B</math> and <math>\rho</math> of <math>B \vdash A</math> such that eliminating the cut on <math>A</math> in |
<math>\AxRule{}\VdotsRule{\pi}{A \vdash B}\AxRule{}\VdotsRule{\rho}{B \vdash A}\LabelRule{\rulename{cut}}\BinRule{B\vdash B}\DisplayProof</math> |
<math>\AxRule{}\VdotsRule{\pi}{A \vdash B}\AxRule{}\VdotsRule{\rho}{B \vdash A}\LabelRule{\rulename{cut}}\BinRule{B\vdash B}\DisplayProof</math> |
||
Revision as of 20:34, 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
.
Some well known isomorphisms of linear logic are the following ones:
-
- …
