# Isomorphism

From LLWiki

Revision as of 21:38, 25 April 2013 by Olivier Laurent (Talk | contribs)

*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.