On the Relation Between Various Negative Translations
Gilda Ferreira, Paulo B. Oliva · 2012
Several proof translations of classical mathematics into intuitionistic (or even minimal) mathematics have been proposed in the literature over the past century. These are normally referred to as negative translations or double-negation translations. Amongst those, the most commonly cited are translations due to Kolmogorov, Godel, 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, Krivine and Godel-Gentzen are minimal elements. A new minimal translation is introduced.