We study how to postpone the application of the reductio ad absurdum rule (RAA) in classical natural deduction. This technique is connected with two normalization strategies for classical logic, due to Prawitz and Seldin, respectively. We introduce a variant of Seldin’s strategy for the postponement of RAA, which induces a negative translation from classical to intuitionistic and minimal logic. Through this translation, Glivenko’s theorem from classical to intuitionistic and minimal logic is proven.

Kolmogorov established the principle of the double negation translation by which to embed Classical Predicate Logic |${\operatorname {CQC}}$| into Intuitionistic Predicate Logic |${\operatorname {IQC}}$|⁠. We show that the obvious generalizations to the Basic Predicate Logic of [3] and to |${\operatorname {BQC}}$| of [12], a proper subsystem of |${\operatorname {IQC}}$|⁠, go through as well. The obvious generalizations of Kuroda’s embedding are shown to be equivalent to the Kolmogorov variant. In our proofs novel nontrivial techniques are needed to overcome the absence of (...) full modus ponens in Basic Predicate Logic. In [3] we argued that |${\operatorname {IQC}}$| is not the logic of constructive mathematics. Our doubts were far from new. New was that we put forward an alternative, |${\operatorname {BQC}}$|⁠. One concern is that |${\operatorname {BQC}}$| is too weak for serious mathematics, or even trivial. This paper is one step to alleviate such concerns. (shrink)