# negative translation

It is well-known that classical propositional logic PL${}_{c}$ can be considered as a subsystem of intuitionistic propositional logic PL${}_{i}$ by translating any wff $A$ in PL${}_{c}$ into $\neg\neg A$ in PL${}_{i}$. According to Glivenko’s theorem, $A$ is a theorem of PL${}_{c}$ iff $\neg\neg A$ is a theorem of PL${}_{i}$. This translation, however, fails to preserve theoremhood in the corresponding predicate logics. For example, if $A$ is of the form $\exists xB$, then $\vdash_{c}A$ no longer implies $\vdash_{i}\neg\neg A$. A number of translations have been devised to overcome this defect. They are collective known as negative translations or double negative translations of classical logic into intuitionistic logic. Below is a list of the most commonly mentioned negative translations:

• Kolmogorov negative translation:

1. (a)

$p^{\circ}:=\neg\neg p$ with $p$ atomic and $\perp^{\circ}:=\perp$

2. (b)

$(A\land B)^{\circ}:=\neg\neg(A^{\circ}\land B^{\circ})$

3. (c)

$(A\lor B)^{\circ}:=\neg\neg(A^{\circ}\lor B^{\circ})$

4. (d)

$(A\to B)^{\circ}:=\neg\neg(A^{\circ}\to B^{\circ})$

5. (e)

$(\forall xA)^{\circ}:=\neg\neg\forall xA^{\circ}$

6. (f)

$(\exists xA)^{\circ}:=\neg\neg\exists xA^{\circ}$

• Godël negative translation:

1. (a)

$p^{-}:=\neg\neg p$ with $p$ atomic and $\perp^{-}:=\perp$

2. (b)

$(A\land B)^{-}:=A^{-}\land B^{-}$

3. (c)

$(A\lor B)^{-}:=\neg\neg(A^{-}\lor B^{-})$

4. (d)

$(A\to B)^{-}:=A^{-}\to B^{-}$

5. (e)

$(\forall xA)^{-}:=\forall xA^{-}$

6. (f)

$(\exists xA)^{-}:=\neg\neg\exists xA^{-}$

• Kuroda negative translation:

1. (a)

$p_{u}:=p$ with $p$ atomic and $\perp_{u}:=\perp$

2. (b)

$(A\land B)_{u}:=A_{u}\land B_{u}$

3. (c)

$(A\lor B)_{u}:=A_{u}\lor B_{u}$

4. (d)

$(A\to B)_{u}:=A_{u}\to B_{u}$

5. (e)

$(\forall xA)_{u}:=\forall x\neg\neg A_{u}$

6. (f)

$(\exists xA)_{u}:=\exists xA_{u}$

And then $A^{u}:=\neg\neg A_{u}$.

• Krivine negative translation:

1. (a)

$p_{r}:=\neg p$ with $p$ atomic and $\perp_{r}:=\neg\perp$

2. (b)

$(A\land B)_{r}:=A_{r}\lor B_{r}$

3. (c)

$(A\lor B)_{r}:=A_{r}\land B_{r}$

4. (d)

$(A\to B)_{r}:=\neg A_{r}\land B_{r}$

5. (e)

$(\forall xA)_{r}:=\exists xA_{r}$

6. (f)

$(\exists xA)_{r}:=\neg\exists x\neg A_{r}$

And then $A^{r}:=\neg A_{r}$.

Remark. It can be shown that for any wff $A$:

 $\vdash_{i}A^{*}\leftrightarrow A^{\#}\qquad\qquad\mbox{and}\qquad\qquad\vdash_% {c}A\quad\mbox{iff}\quad\vdash_{i}A^{*}$

where $*,\#\in\{\circ,-,u,r\}$.

 Title negative translation Canonical name NegativeTranslation Date of creation 2013-03-22 19:35:48 Last modified on 2013-03-22 19:35:48 Owner CWoo (3771) Last modified by CWoo (3771) Numerical id 9 Author CWoo (3771) Entry type Definition Classification msc 03B20 Classification msc 03F55 Synonym double negative translation Defines Kolmogorov negative translation Defines Godel negative translation Defines Kuroda negative translation Defines Krivine negative translation \@unrecurse