http://140-77-166-78.cprapid.com/mediawiki/index.php?action=history&feed=atom&title=Translations_of_classical_logic
Translations of classical logic - Revision history
2026-04-12T07:36:41Z
Revision history for this page on the wiki
MediaWiki 1.19.20+dfsg-0+deb7u3
http://140-77-166-78.cprapid.com/mediawiki/index.php?title=Translations_of_classical_logic&diff=415&oldid=prev
Olivier Laurent: Q-translation added
2009-10-05T21:11:13Z
<p>Q-translation added</p>
<a href="http://140-77-166-78.cprapid.com/mediawiki/index.php?title=Translations_of_classical_logic&diff=415&oldid=410">Show changes</a>
Olivier Laurent
http://140-77-166-78.cprapid.com/mediawiki/index.php?title=Translations_of_classical_logic&diff=410&oldid=prev
Olivier Laurent: T-translation
2009-09-21T21:04:25Z
<p>T-translation</p>
<p><b>New page</b></p><div>== T-translation <math>A\imp B \mapsto \oc{\wn{A}}\limp\wn{B}</math> ==<br />
<br />
Formulas are translated as:<br />
<br />
<math><br />
\begin{array}{rcl}<br />
X^T & = & X \\<br />
(A\imp B)^T & = & \oc{\wn{A^T}}\limp\wn{B^T} \\<br />
(A\wedge B)^T & = & \wn{A^T} \with \wn{B^T} \\<br />
T^T & = & \top \\<br />
(A\vee B)^T & = & \wn{A^T}\parr\wn{B^T} \\<br />
F^T & = & \bot \\<br />
(\neg A)^T & = & \wn{\oc{(A^T)\orth}} \\<br />
(\forall\xi A)^T & = & \forall\xi \wn{A^T} \\<br />
(\exists\xi A)^T & = & \exists\xi \oc{\wn{A^T}}<br />
\end{array}<br />
</math><br />
<br />
This is extended to sequents by <math>(\Gamma\vdash\Delta)^T = \oc{\wn{\Gamma^T}}\vdash\wn{\Delta^T}</math>.<br />
<br />
This allows one to translate the rules of classical logic into linear logic:<br />
<br />
<math><br />
\LabelRule{\rulename{ax}}<br />
\NulRule{A\vdash A}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\LabelRule{\rulename{ax}}<br />
\NulRule{\wn{A^T}\vdash\wn{A^T}}<br />
\LabelRule{\oc L}<br />
\UnaRule{\oc{\wn{A^T}}\vdash\wn{A^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma\vdash A,\Delta}<br />
\AxRule{\Gamma',A\vdash\Delta'}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\Gamma,\Gamma'\vdash\Delta,\Delta'}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}}\vdash\wn{A^T},\wn{\Delta^T}}<br />
\LabelRule{\oc R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash\oc{\wn{A^T}},\wn{\Delta^T}}<br />
\AxRule{\oc{\wn{\Gamma'^T}},\oc{\wn{A^T}}\vdash\wn{\Delta'^T}}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\oc{\wn{\Gamma^T}},\oc{\wn{\Gamma'^T}}\vdash\wn{\Delta^T},\wn{\Delta'^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma,A,A\vdash\Delta}<br />
\LabelRule{c L}<br />
\UnaRule{\Gamma,A\vdash\Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}},\oc{\wn{A^T}},\oc{\wn{A^T}}\vdash\wn{\Delta^T}}<br />
\LabelRule{\oc c L}<br />
\UnaRule{\oc{\wn{\Gamma^T}},\oc{\wn{A^T}}\vdash\wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma\vdash A,A,\Delta}<br />
\LabelRule{c R}<br />
\UnaRule{\Gamma\vdash A,\Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}}\vdash\wn{A^T},\wn{A^T},\wn{\Delta^T}}<br />
\LabelRule{\wn c R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash\wn{A^T},\wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma\vdash\Delta}<br />
\LabelRule{w L}<br />
\UnaRule{\Gamma,A\vdash\Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}}\vdash\wn{\Delta^T}}<br />
\LabelRule{\oc w L}<br />
\UnaRule{\oc{\wn{\Gamma^T}},\oc{\wn{A^T}}\vdash\wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma\vdash\Delta}<br />
\LabelRule{w R}<br />
\UnaRule{\Gamma\vdash A,\Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}}\vdash\wn{\Delta^T}}<br />
\LabelRule{\wn w R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash\wn{A^T},\wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma,A\vdash B,\Delta}<br />
\LabelRule{\imp R}<br />
\UnaRule{\Gamma\vdash A\imp B,\Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}},\oc{\wn{A^T}}\vdash\wn{B^T},\wn{\Delta^T}}<br />
\LabelRule{\limp R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \oc{\wn{A^T}}\limp\wn{B^T},\wn{\Delta^T}}<br />
\LabelRule{\wn d R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \wn{(\oc{\wn{A^T}}\limp\wn{B^T})},\wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma\vdash A,\Delta}<br />
\AxRule{\Gamma',B\vdash\Delta'}<br />
\LabelRule{\imp L}<br />
\BinRule{\Gamma,\Gamma',A\imp B\vdash\Delta,\Delta'}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}}\vdash\wn{A^T},\wn{\Delta^T}}<br />
\LabelRule{\oc R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash\oc{\wn{A^T}},\wn{\Delta^T}}<br />
\LabelRule{\rulename{ax}}<br />
\NulRule{\wn{B^T}\vdash\wn{B^T}}<br />
\LabelRule{\limp L}<br />
\BinRule{\oc{\wn{\Gamma^T}},\oc{\wn{A^T}}\limp\wn{B^T}\vdash\wn{B^T},\wn{\Delta^T}}<br />
\LabelRule{\wn L}<br />
\UnaRule{\oc{\wn{\Gamma^T}},\wn{(\oc{\wn{A^T}}\limp\wn{B^T})}\vdash\wn{B^T},\wn{\Delta^T}}<br />
\LabelRule{\oc d L}<br />
\UnaRule{\oc{\wn{\Gamma^T}},\oc{\wn{(\oc{\wn{A^T}}\limp\wn{B^T})}}\vdash\wn{B^T},\wn{\Delta^T}}<br />
\LabelRule{\oc R}<br />
\UnaRule{\oc{\wn{\Gamma^T}},\oc{\wn{(\oc{\wn{A^T}}\limp\wn{B^T})}}\vdash\oc{\wn{B^T}},\wn{\Delta^T}}<br />
\AxRule{\oc{\wn{\Gamma'^T}},\oc{\wn{B^T}}\vdash\wn{\Delta'^T}}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\oc{\wn{\Gamma^T}},\oc{\wn{\Gamma'^T}},\oc{\wn{(\oc{\wn{A^T}}\limp\wn{B^T})}}\vdash\wn{\Delta^T},\wn{\Delta'^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma\vdash A,\Delta}<br />
\AxRule{\Gamma\vdash B,\Delta}<br />
\LabelRule{\wedge R}<br />
\BinRule{\Gamma\vdash A\wedge B,\Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}}\vdash \wn{A^T},\wn{\Delta^T}}<br />
\AxRule{\oc{\wn{\Gamma^T}}\vdash \wn{B^T},\wn{\Delta^T}}<br />
\LabelRule{\with R}<br />
\BinRule{\oc{\wn{\Gamma^T}}\vdash \wn{A^T}\with \wn{B^T},\wn{\Delta^T}}<br />
\LabelRule{\wn d R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \wn{(\wn{A^T}\with \wn{B^T})},\wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma,A\vdash \Delta}<br />
\LabelRule{\wedge_1 L}<br />
\UnaRule{\Gamma,A\wedge B\vdash \Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\LabelRule{\rulename{ax}}<br />
\NulRule{\wn{A^T}\vdash \wn{A^T}}<br />
\LabelRule{\with_1 L}<br />
\UnaRule{\wn{A^T}\with \wn{B^T}\vdash \wn{A^T}}<br />
\LabelRule{\wn L}<br />
\UnaRule{\wn{(\wn{A^T}\with \wn{B^T})}\vdash \wn{A^T}}<br />
\LabelRule{\oc d L}<br />
\UnaRule{\oc{\wn{(\wn{A^T}\with \wn{B^T})}}\vdash \wn{A^T}}<br />
\LabelRule{\oc R}<br />
\UnaRule{\oc{\wn{(\wn{A^T}\with \wn{B^T})}}\vdash \oc{\wn{A^T}}}<br />
\AxRule{\oc{\wn{\Gamma^T}},\oc{\wn{A^T}}\vdash \wn{\Delta^T}}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\oc{\wn{\Gamma^T}},\oc{\wn{(\wn{A^T}\with \wn{B^T})}}\vdash \wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\LabelRule{T R}<br />
\NulRule{\Gamma\vdash T,\Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\LabelRule{\top R}<br />
\NulRule{\oc{\wn{\Gamma^T}}\vdash \top,\wn{\Delta^T}}<br />
\LabelRule{\wn d R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \wn{\top},\wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma\vdash A,B,\Delta}<br />
\LabelRule{\vee R}<br />
\UnaRule{\Gamma\vdash A\vee B,\Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}}\vdash \wn{A^T},\wn{B^T},\wn{\Delta^T}}<br />
\LabelRule{\parr R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \wn{A^T}\parr\wn{B^T},\wn{\Delta^T}}<br />
\LabelRule{\wn d R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \wn{(\wn{A^T}\parr\wn{B^T})},\wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma,A\vdash \Delta}<br />
\AxRule{\Gamma',B\vdash \Delta'}<br />
\LabelRule{\vee L}<br />
\BinRule{\Gamma,\Gamma',A\vee B\vdash \Delta,\Delta'}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\LabelRule{\rulename{ax}}<br />
\NulRule{\wn{A^T}\vdash \wn{A^T}}<br />
\LabelRule{\rulename{ax}}<br />
\NulRule{\wn{B^T}\vdash \wn{B^T}}<br />
\LabelRule{\parr L}<br />
\BinRule{\wn{A^T}\parr \wn{B^T}\vdash \wn{A^T},\wn{B^T}}<br />
\LabelRule{\wn L}<br />
\UnaRule{\wn{(\wn{A^T}\parr \wn{B^T})}\vdash \wn{A^T},\wn{B^T}}<br />
\LabelRule{\oc d L}<br />
\UnaRule{\oc{\wn{(\wn{A^T}\parr \wn{B^T})}}\vdash \wn{A^T},\wn{B^T}}<br />
\LabelRule{\oc R}<br />
\UnaRule{\oc{\wn{(\wn{A^T}\parr \wn{B^T})}}\vdash \wn{A^T},\oc{\wn{B^T}}}<br />
\AxRule{\oc{\wn{\Gamma'^T}},\oc{\wn{B^T}}\vdash \wn{\Delta'^T}}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\oc{\wn{\Gamma'^T}},\oc{\wn{(\wn{A^T}\parr \wn{B^T})}}\vdash \wn{A^T},\wn{\Delta'^T}}<br />
\LabelRule{\oc R}<br />
\UnaRule{\oc{\wn{\Gamma'^T}},\oc{\wn{(\wn{A^T}\parr \wn{B^T})}}\vdash \oc{\wn{A^T}},\wn{\Delta'^T}}<br />
\AxRule{\oc{\wn{\Gamma^T}},\oc{\wn{A^T}}\vdash \wn{\Delta^T}}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\oc{\wn{\Gamma^T}},\oc{\wn{\Gamma'^T}},\oc{\wn{(\wn{A^T}\parr \wn{B^T})}}\vdash \wn{\Delta^T},\wn{\Delta'^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma\vdash \Delta}<br />
\LabelRule{F R}<br />
\UnaRule{\Gamma\vdash F,\Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}}\vdash \wn{\Delta^T}}<br />
\LabelRule{\bot R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \bot,\wn{\Delta^T}}<br />
\LabelRule{\wn R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \wn{\bot},\wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\LabelRule{F L}<br />
\NulRule{F\vdash {}}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\LabelRule{\bot L}<br />
\NulRule{\bot\vdash {}}<br />
\LabelRule{\wn L}<br />
\UnaRule{\wn{\bot}\vdash {}}<br />
\LabelRule{\oc d L}<br />
\UnaRule{\oc{\wn{\bot}}\vdash {}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma,A\vdash \Delta}<br />
\LabelRule{\neg R}<br />
\UnaRule{\Gamma\vdash \neg A,\Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}},\oc{\wn{A^T}}\vdash \wn{\Delta^T}}<br />
\LabelRule{(.)\orth R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \wn{\oc{(A^T)\orth}},\wn{\Delta^T}}<br />
\LabelRule{\wn d R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \wn{\wn{\oc{(A^T)\orth}}},\wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma\vdash A,\Delta}<br />
\LabelRule{\neg L}<br />
\UnaRule{\Gamma,\neg A\vdash \Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}}\vdash \wn{A^T},\wn{\Delta^T}}<br />
\LabelRule{(.)\orth L}<br />
\UnaRule{\oc{\wn{\Gamma^T}},\oc{(A^T)\orth}\vdash \wn{\Delta^T}}<br />
\LabelRule{\wn L}<br />
\UnaRule{\oc{\wn{\Gamma^T}},\wn{\oc{(A^T)\orth}}\vdash \wn{\Delta^T}}<br />
\LabelRule{\wn L}<br />
\UnaRule{\oc{\wn{\Gamma^T}},\wn{\wn{\oc{(A^T)\orth}}}\vdash \wn{\Delta^T}}<br />
\LabelRule{\oc d L}<br />
\UnaRule{\oc{\wn{\Gamma^T}},\oc{\wn{\wn{\oc{(A^T)\orth}}}}\vdash \wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma\vdash A,\Delta}<br />
\LabelRule{\forall R}<br />
\UnaRule{\Gamma\vdash \forall\xi A,\Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}}\vdash \wn{A^T},\wn{\Delta^T}}<br />
\LabelRule{\forall R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \forall\xi \wn{A^T},\wn{\Delta^T}}<br />
\LabelRule{\wn d R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \wn{\forall\xi \wn{A^T}},\wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma,A[\tau/\xi]\vdash \Delta}<br />
\LabelRule{\forall L}<br />
\UnaRule{\Gamma,\forall\xi A\vdash \Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\LabelRule{\rulename{ax}}<br />
\NulRule{\wn{A^T}[\tau^T/\xi]\vdash \wn{A^T}[\tau^T/\xi]}<br />
\LabelRule{\forall L}<br />
\UnaRule{\forall\xi \wn{A^T}\vdash \wn{A^T}[\tau^T/\xi]}<br />
\LabelRule{\wn L}<br />
\UnaRule{\wn{\forall\xi \wn{A^T}}\vdash \wn{A^T}[\tau^T/\xi]}<br />
\LabelRule{\oc d L}<br />
\UnaRule{\oc{\wn{\forall\xi \wn{A^T}}}\vdash \wn{A^T}[\tau^T/\xi]}<br />
\LabelRule{\oc R}<br />
\UnaRule{\oc{\wn{\forall\xi \wn{A^T}}}\vdash \oc{\wn{A^T}}[\tau^T/\xi]}<br />
\AxRule{\oc{\wn{\Gamma^T}},\oc{\wn{(A^T[\tau^T/\xi])}}\vdash \wn{\Delta^T}}<br />
\LabelRule{\rulename{cut}}<br />
\BinRule{\oc{\wn{\Gamma^T}},\oc{\wn{\forall\xi \wn{A^T}}}\vdash \wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma\vdash A[\tau/\xi],\Delta}<br />
\LabelRule{\exists R}<br />
\UnaRule{\Gamma\vdash \exists\xi A,\Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}}\vdash \wn{A^T[\tau^T/\xi]},\wn{\Delta^T}}<br />
\LabelRule{\oc R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \oc{\wn{A^T[\tau^T/\xi]}},\wn{\Delta^T}}<br />
\LabelRule{\exists R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \exists\xi \oc{\wn{A^T}},\wn{\Delta^T}}<br />
\LabelRule{\wn d R}<br />
\UnaRule{\oc{\wn{\Gamma^T}}\vdash \wn{\exists\xi \oc{\wn{A^T}}},\wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
<br /><br />
<br />
<math><br />
\AxRule{\Gamma,A\vdash \Delta}<br />
\LabelRule{\exists L}<br />
\UnaRule{\Gamma,\exists\xi A\vdash \Delta}<br />
\DisplayProof<br />
\qquad\mapsto\qquad<br />
\AxRule{\oc{\wn{\Gamma^T}},\oc{\wn{A^T}}\vdash \wn{\Delta^T}}<br />
\LabelRule{\exists L}<br />
\UnaRule{\oc{\wn{\Gamma^T}},\exists\xi\oc{\wn{A^T}}\vdash \wn{\Delta^T}}<br />
\LabelRule{\wn L}<br />
\UnaRule{\oc{\wn{\Gamma^T}},\wn{\exists\xi\oc{\wn{A^T}}}\vdash \wn{\Delta^T}}<br />
\LabelRule{\oc d L}<br />
\UnaRule{\oc{\wn{\Gamma^T}},\oc{\wn{\exists\xi\oc{\wn{A^T}}}}\vdash \wn{\Delta^T}}<br />
\DisplayProof<br />
</math><br />
<br />
=== Alternative presentation ===<br />
<br />
It is also possible to define <math>A^{\overline{T}}</math> by:<br />
<br />
<math><br />
\begin{array}{rcl}<br />
X^{\overline{T}} & = & \wn{X} \\<br />
(A\imp B)^{\overline{T}} & = & \wn{(\oc{A^{\overline{T}}}\limp B^{\overline{T}})} \\<br />
(A\wedge B)^{\overline{T}} & = & \wn{(A^{\overline{T}} \with B^{\overline{T}})} \\<br />
T^{\overline{T}} & = & \wn{\top} \\<br />
(A\vee B)^{\overline{T}} & = & \wn{(A^{\overline{T}}\parr B^{\overline{T}})} \\<br />
F^{\overline{T}} & = & \wn{\bot} \\<br />
(\neg A)^{\overline{T}} & = & \wn{\wn{(A^{\overline{T}})\orth}} \\<br />
(\forall\xi A)^{\overline{T}} & = & \wn{\forall\xi A^{\overline{T}}} \\<br />
(\exists\xi A)^{\overline{T}} & = & \wn{\exists\xi \oc{A^{\overline{T}}}}<br />
\end{array}<br />
</math><br />
<br />
If we define <math>(\Gamma\vdash\Delta)^{\overline{T}} = \oc{\Gamma^{\overline{T}}}\vdash \Delta^{\overline{T}}</math>, we have <math>(\Gamma\vdash\Delta)^{\overline{T}} = (\Gamma\vdash\Delta)^T</math> and thus we obtain the same translation of proofs.</div>
Olivier Laurent