Translations of intuitionistic logic - Revision history

Olivier Laurent: /* Call-by-value translation A\imp B \mapsto \oc{(A\limp B)} */ T L rule

2009-10-05T20:25:25Z

‎Call-by-value translation A\imp B \mapsto \oc{(A\limp B)}: T L rule

2009-10-05T20:08:51Z

‎Call-by-value Girard's translation A\imp B \mapsto \oc{(A\limp B)}: typos

2009-10-05T20:07:16Z

‎Call-by-value translation A\imp B \mapsto \oc{(A\limp B)}: typos

2009-10-05T20:05:16Z

‎Call-by-name Girard's translation A\imp B \mapsto \oc{A}\limp B: typo

2009-03-24T22:41:41Z

‎Call-by-value Girard's translation A\imp B \mapsto \oc{(A\limp B)}

2009-03-24T22:40:35Z

‎Call-by-value translation A\imp B \mapsto \oc{(A\limp B)}

2009-03-24T22:39:17Z

‎Call-by-value Girard's translation A\imp B \mapsto \oc{(A\limp B)}

2009-03-24T22:38:30Z

‎Call-by-value translation A\imp B \mapsto \oc{(A\limp B)}

2009-03-06T14:46:40Z

‎Call-by-value Girard's translation A\imp B \mapsto \oc{(A\limp B)}: modified rule names

2009-02-12T22:19:20Z

‎Call-by-value Girard's translation A\imp B \mapsto \oc{(A\limp B)}: use of \rulename

@@ Line 444: / Line 444: @@
 \LabelRule{\oc R}
 \UnaRule{{}\vdash \oc{\one}}
 \DisplayProof
 </math>

@@ Line 689: / Line 689: @@
 \LabelRule{\limp L}
 \BinRule{\Gamma^w,\Delta^w,A^w\limp B^w\vdash C^w}
-\LabelRule{\oc L}
+\LabelRule{\oc d L}
 \UnaRule{\Gamma^w,\Delta^w,\oc{(A^w\limp B^w)}\vdash C^w}
 \DisplayProof
@@ Line 808: / Line 808: @@
 \LabelRule{\forall L}
 \UnaRule{\Gamma^w,\forall\xi A^w\vdash C^w}
-\LabelRule{\oc L}
+\LabelRule{\oc d L}
 \UnaRule{\Gamma^w,\oc{\forall\xi A^w}\vdash C^w}
 \DisplayProof

@@ Line 394: / Line 394: @@
 \LabelRule{\limp L}
 \BinRule{\Gamma^v,\Delta^v,A^v\limp B^v\vdash C^v}
-\LabelRule{\oc L}
+\LabelRule{\oc d L}
 \UnaRule{\Gamma^v,\Delta^v,\oc{(A^v\limp B^v)}\vdash C^v}
 \DisplayProof
@@ Line 428: / Line 428: @@
 \LabelRule{\tens L}
 \UnaRule{\Gamma^v,A^v\tens B^v\vdash C^v}
-\LabelRule{\oc L}
+\LabelRule{\oc d L}
 \UnaRule{\Gamma^v,\oc{(A^v\tens B^v)}\vdash C^v}
 \DisplayProof
@@ Line 524: / Line 524: @@
 \LabelRule{\forall L}
 \UnaRule{\Gamma^v,\forall\xi A^v\vdash C^v}
-\LabelRule{\oc L}
+\LabelRule{\oc d L}
 \UnaRule{\Gamma^v,\oc{\forall\xi A^v}\vdash C^v}
 \DisplayProof

@@ Line 31: / Line 31: @@
 \LabelRule{\rulename{ax}}
 \NulRule{A^n\vdash A^n}
-\LabelRule{\oc L}
+\LabelRule{\oc d L}
 \UnaRule{\oc{A^n}\vdash A^n}
 \DisplayProof

@@ Line 809: / Line 809: @@
 \UnaRule{\Gamma^w,\forall\xi A^w\vdash C^w}
 \LabelRule{\oc L}
-\UnaRule{\Gamma^w,\oc{(\forall\xi A^w)}\vdash C^w}
+\UnaRule{\Gamma^w,\oc{\forall\xi A^w}\vdash C^w}
 \DisplayProof
 </math>

@@ Line 595: / Line 595: @@
 (A\vee B)^w & = & A^w\plus B^w \\
 F^w & = & \zero \\
-(\forall\xi A)^w & = & \oc{(\forall\xi A^w)} \\
+(\forall\xi A)^w & = & \oc{\forall\xi A^w} \\
 (\exists\xi A)^w & = & \exists\xi A^w
 \end{array}

@@ Line 300: / Line 300: @@
 (A\vee B)^v & = & \oc{(A^v\plus B^v)} \\
 F^v & = & \oc{\zero} \\
-(\forall\xi A)^v & = & \oc{(\forall\xi A^v)} \\
+(\forall\xi A)^v & = & \oc{\forall\xi A^v} \\
-(\exists\xi A)^v & = & \oc{(\exists\xi A^v)}
+(\exists\xi A)^v & = & \oc{\exists\xi A^v}
 \end{array}
 </math>

@@ Line 671: / Line 671: @@
 \LabelRule{\limp R}
 \UnaRule{\Gamma^w\vdash A^w\limp B^w}
-\LabelRule{\oc R}
+\LabelRule{+ \oc R}
 \UnaRule{\Gamma^w\vdash \oc{(A^w\limp B^w)}}
 \DisplayProof
@@ Line 789: / Line 789: @@
 \LabelRule{\forall R}
 \UnaRule{\Gamma^w\vdash \forall\xi A^w}
-\LabelRule{\oc R}
+\LabelRule{+ \oc R}
 \UnaRule{\Gamma^w\vdash \oc{\forall\xi A^w}}
 \DisplayProof

@@ Line 607: / Line 607: @@
 <math>
-\LabelRule{\textit{ax}}
+\LabelRule{\rulename{ax}}
 \NulRule{A\vdash A}
 \DisplayProof
 \qquad\mapsto\qquad
-\LabelRule{\textit{ax}}
+\LabelRule{\rulename{ax}}
 \NulRule{A^w\vdash A^w}
 \DisplayProof
@@ Line 621: / Line 621: @@
 \AxRule{\Gamma\vdash A}
 \AxRule{\Delta,A\vdash B}
-\LabelRule{\textit{cut}}
+\LabelRule{\rulename{cut}}
 \BinRule{\Gamma,\Delta\vdash B}
 \DisplayProof
@@ Line 627: / Line 627: @@
 \AxRule{\Gamma^w\vdash A^w}
 \AxRule{\Delta^w,A^w\vdash B^w}
-\LabelRule{\textit{cut}}
+\LabelRule{\rulename{cut}}
 \BinRule{\Gamma^w,\Delta^w\vdash B^w}
 \DisplayProof
@@ Line 841: / Line 841: @@
 \DisplayProof
 </math>
 == References ==