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