Postponement of raa and Glivenko's theorem, revisited (extended version)

TL;DR

This paper explores techniques for postponing the application of the reduction ad absurdum rule in classical natural deduction, connecting it with normalization strategies and using it to derive variants of Glivenko's theorem for intuitionistic and minimal logic.

Contribution

It introduces a variant of Seldin's strategy for postponing raa and demonstrates its use in deriving a negative translation akin to Kuroda's, leading to a proof of Glivenko's theorem.

Findings

Postponement of raa linked to normalization strategies.

A variant of Seldin's strategy induces a negative translation.

Glivenko's theorem proven for intuitionistic and minimal logic.

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.