arXiv · 1710.08854
Postponement of raa and Glivenko's theorem, revisited (extended version)
Abstract
This article focuses on the technique of postponing the application of the reduction ad absurdum rule (raa) in classical natural deduction. First, it is shown how this technique is connected with two normalization strategies for classical logic: one given by Prawitz, and the other by Seldin. Secondly, a variant of Seldin's strategy for the postponement of raa is proposed, and the similarities with Prawitz's approach are investigated. In particular, it is shown that, as for Prawitz, it is possible to use this variant of Seldin's strategy in order to induce a negative translation from classical to intuitionistic and minimal logic, which is nothing but a variant of Kuroda's translation. Through this translation, Glivenko's theorem for intuitionistic and minimal logic is proven.
Explore related subjects
Keep this discovery
Giulio Guerrieri, Alberto Naibo. 2017-10-24. Postponement of raa and Glivenko's theorem, revisited (extended version). https://arxiv.org/abs/1710.08854
Cite the original work for its findings. Save a collection to share your selection of sources.