On Various Negative Translations

TL;DR

This paper introduces a framework to compare various classical-to-intuitionistic proof translations, revealing their relationships and proposing new minimal translations within a structured hierarchy.

Contribution

It defines a modular simplification framework to relate different negative translations and introduces two new minimal translations.

Findings

Kuroda and Krivine translations are minimal in the hierarchy.

A partial order between translations is established.

Two new minimal translations are proposed.

Abstract

Several proof translations of classical mathematics into intuitionistic mathematics have been proposed 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 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 and Krivine are minimal elements. Two new minimal translations are introduced, with Godel and Gentzen translations sitting in between Kolmogorov and one of these new translations.