View source for Translations of classical logic

=== Alternative presentation ===

It is also possible to define <math>A^{\underline{Q}}</math> as the primitive construction.

<math>
\begin{array}{rcl}
X^{\underline{Q}} & = & X \\
(A\imp B)^{\underline{Q}} & = & \oc{A^{\underline{Q}}}\limp\wn{\oc{B^{\underline{Q}}}} \\
(A\wedge B)^{\underline{Q}} & = & \oc{A^{\underline{Q}}}\tens\oc{B^{\underline{Q}}} \\
T^{\underline{Q}} & = & \one \\
(A\vee B)^{\underline{Q}} & = & \oc{A^{\underline{Q}}}\plus\oc{B^{\underline{Q}}} \\
F^{\underline{Q}} & = & \zero \\
(\neg A)^{\underline{Q}} & = & \wn{(A^{\underline{Q}})\orth} \\
(\forall\xi A)^{\underline{Q}} & = & \forall\xi \wn{\oc{A^{\underline{Q}}}} \\
(\exists\xi A)^{\underline{Q}} & = & \exists\xi \oc{A^{\underline{Q}}}
\end{array}
</math>

If we define <math>(\Gamma\vdash\Delta)^{\underline{Q}} = \oc{\Gamma^{\underline{Q}}}\vdash\wn{\oc{\Delta^{\underline{Q}}}}</math>, we have <math>(\Gamma\vdash\Delta)^{\underline{Q}} = (\Gamma\vdash\Delta)^Q</math> and thus we obtain the same translation of proofs.