Computer Science – Logic in Computer Science
Scientific paper
2011-01-28
EPTCS 47, 2011, pp. 21-33
Computer Science
Logic in Computer Science
In Proceedings CL&C 2010, arXiv:1101.5200
Scientific paper
10.4204/EPTCS.47.4
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.
Ferreira Gilda
Oliva Paulo
No associations
LandOfFree
On Various Negative Translations does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with On Various Negative Translations, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On Various Negative Translations will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-551449