On Various Negative Translations
Gilda Ferreira, Paulo Oliva

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
