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 $\eg\eg A$ in PL ${}_{i}$ . According to Glivenko’s theorem, $A$ is a theorem of PL ${}_{c}$ iff $\eg\eg 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}\eg\eg 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}:=\eg\eg p$ with $p$ atomic and $\\perp^{\\circ}:=\\perp$
2. (b)
  $(A\\land B)^{\\circ}:=\eg\eg(A^{\\circ}\\land B^{\\circ})$
3. (c)
  $(A\\lor B)^{\\circ}:=\eg\eg(A^{\\circ}\\lor B^{\\circ})$
4. (d)
  $(A\\to B)^{\\circ}:=\eg\eg(A^{\\circ}\\to B^{\\circ})$
5. (e)
  $(\\forall xA)^{\\circ}:=\eg\eg\\forall xA^{\\circ}$
6. (f)
  $(\\exists xA)^{\\circ}:=\eg\eg\\exists xA^{\\circ}$
•
Godël negative translation:
1. (a)
  $p^{-}:=\eg\eg p$ with $p$ atomic and $\\perp^{-}:=\\perp$
2. (b)
  $(A\\land B)^{-}:=A^{-}\\land B^{-}$
3. (c)
  $(A\\lor B)^{-}:=\eg\eg(A^{-}\\lor B^{-})$
4. (d)
  $(A\\to B)^{-}:=A^{-}\\to B^{-}$
5. (e)
  $(\\forall xA)^{-}:=\\forall xA^{-}$
6. (f)
  $(\\exists xA)^{-}:=\eg\eg\\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\eg\eg A_{u}$
6. (f)
  $(\\exists xA)_{u}:=\\exists xA_{u}$
And then $A^{u}:=\eg\eg A_{u}$ .
•
Krivine negative translation:
1. (a)
  $p_{r}:=\eg p$ with $p$ atomic and $\\perp_{r}:=\eg\\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}:=\eg A_{r}\\land B_{r}$
5. (e)
  $(\\forall xA)_{r}:=\\exists xA_{r}$
6. (f)
  $(\\exists xA)_{r}:=\eg\\exists x\eg A_{r}$
And then $A^{r}:=\eg 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\\}$ .