Isomorphism - Revision history

Olivier Laurent: Link to list of isomorphisms

2013-04-25T19:38:11Z

Link to list of isomorphisms

Olivier Laurent: notation for isomorphisms

2013-04-25T19:34:31Z

notation for isomorphisms

Lionel Vaux: added template stub

2009-10-16T13:38:52Z

added template stub

Lionel Vaux: stub

2009-10-16T12:30:23Z

stub

New page

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

<math>\AxRule{}\VdotsRule{\pi}{A \vdash B}\AxRule{}\VdotsRule{\rho}{B \vdash A}\LabelRule{\rulename{cut}}\BinRule{B\vdash B}\DisplayProof</math>

leads to an [[Sequent_calculus#Expansion_of_identities|<math>\eta</math>-expansion]] of

<math>\LabelRule{\rulename{ax}}\NulRule{B\vdash B}\DisplayProof</math>,

and eliminating the cut on <math>B</math> in

<math>\AxRule{}\VdotsRule{\pi}{A \vdash B}\AxRule{}\VdotsRule{\rho}{B \vdash A}\LabelRule{\rulename{cut}}\BinRule{A\vdash A}\DisplayProof</math>

leads to an [[Sequent_calculus#Expansion_of_identities|<math>\eta</math>-expansion]] of

<math>\LabelRule{\rulename{ax}}\NulRule{A\vdash A}\DisplayProof</math>.

Some well known isomorphisms of linear logic are the following ones:
* <math>A\tens B \limp C \cong A\limp B \limp C</math>
* …

← Older revision		Revision as of 19:38, 25 April 2013
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>
−	* …

@@ Line 1: / Line 1: @@
 {{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>

← Older revision		Revision as of 13:38, 16 October 2009
Line 1:		Line 1:
		+	{{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, 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