Abstract
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 (a variant of Kuroda’s one) from classical to intuitionistic and minimal logic. Through this translation, Glivenko’s theorem from classical to intuitionistic and minimal logic is proven.
Original language | English |
---|---|
Pages (from-to) | 109-144 |
Number of pages | 36 |
Journal | Studia Logica |
Volume | 107 |
Issue number | 1 |
Early online date | 9 Mar 2018 |
DOIs | |
Publication status | Published - 15 Feb 2019 |
Keywords
- Natural deduction
- Negative translation
- Proof theory
- Reductio ad absurdum.
ASJC Scopus subject areas
- Logic
- History and Philosophy of Science