On various negative translations
Gilda Ferreira, Paulo B. Oliva · 2010
Several proof translations of classical mathematics into intuitionistic mathematics have been pro-posed in the literature over the past century. These are normally referred to as negative translations or double-negation translations. Among those, the most commonly cited are translations due to Kol-mogorov, Gödel, Gentzen, Kuroda and Krivine (in chronological order). In this paper we propose a framework for explaining how these different translations are related to each other. More precisely, we define a notion of a (modular) simplification starting from Kolmogorov translation, which leads to a partial order between different negative translations. In this derived ordering, Kuroda and Kriv-ine are minimal elements. Two new minimal translations are introduced, with Gödel and Gentzen translations sitting in between Kolmogorov and one of these new translations. 1