Studia Logica:1-36 (forthcoming)

Alberto Naibo
University of Paris 1 Panthéon-Sorbonne
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.
Keywords proof theory  natural deduction  negative translation  reduction ad absurdum
Categories (categorize this paper)
DOI 10.1007/s11225-017-9781-5
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 64,262
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Glivenko Theorems for Substructural Logics Over FL.Nikolaos Galatos & Hiroakira Ono - 2006 - Journal of Symbolic Logic 71 (4):1353 - 1384.
Glivenko Theorems Revisited.Hiroakira Ono - 2010 - Annals of Pure and Applied Logic 161 (2):246-250.
Glivenko and Kuroda for Simple Type Theory.Chad E. Brown & Christine Rizkallah - 2014 - Journal of Symbolic Logic 79 (2):485-495.
Subminimal Logic and Weak Algebras.Rodolfo Ertola & Marta Sagastume - 2009 - Reports on Mathematical Logic:153-166.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Glivenko Theorems for Substructural Logics Over FL.Nikolaos Galatos & Hiroakira Ono - 2006 - Journal of Symbolic Logic 71 (4):1353 - 1384.
On the Proof Theory of the Intermediate Logic MH.Jonathan P. Seldin - 1986 - Journal of Symbolic Logic 51 (3):626-647.
A Binary-Conclusion Natural Deduction System.K. Fujita - 1999 - Logic Journal of the IGPL 7 (4):517-545.
A Proof-Search Procedure for Intuitionistic Propositional Logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
Non-Fregean Propositional Logic with Quantifiers.Joanna Golińska-Pilarek & Taneli Huuskonen - 2016 - Notre Dame Journal of Formal Logic 57 (2):249-279.
Uniqueness of Normal Proofs in Implicational Intuitionistic Logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.


Added to PP index

Total views
24 ( #457,816 of 2,455,764 )

Recent downloads (6 months)
1 ( #449,201 of 2,455,764 )

How can I increase my downloads?


My notes