Studia Logica

, Volume 107, Issue 1, pp 109–144 | Cite as

Postponement of \(\mathsf {raa}\) and Glivenko’s Theorem, Revisited

  • Giulio GuerrieriEmail author
  • Alberto Naibo


We study how to postpone the application of the reductio ad absurdum rule (\(\mathsf {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 \(\mathsf {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.


Proof theory Natural deduction Negative translation Reductio ad absurdum. 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ariola, Z. M., H. Herbelin, and A. Sabry, A proof-theoretic foundation of abortive continuations, Higher-Order and Symbolic Computation 20(4):403–429, 2007.CrossRefGoogle Scholar
  2. 2.
    Brown, C. E., and C. Rizkallah, Glivenko and Kuroda for Simple Type Theory, The Journal of Symbolic Logic 79(2):485–495, 2014.CrossRefGoogle Scholar
  3. 3.
    Ertola, R., and M. Sagastume, Subminimal logic and weak algebras, Reports on Mathematical Logic 44:153–166, 2009.Google Scholar
  4. 4.
    Espíndola, C., A short proof of Glivenko theorems for intermediate predicate logics, Archive for Mathematical Logic 52(7):823–826, 2013.CrossRefGoogle Scholar
  5. 5.
    Farahani, H., and H. Ono, Glivenko theorems and negative translations in substructural predicate logics, Archive for Mathematical Logic 51(7):695–707, 2012.CrossRefGoogle Scholar
  6. 6.
    Ferreira, G., and P. Oliva, On the relation between various negative translations, in U. Berger, H. Diener, P. Schuster, and M. Seisenberger (eds.), Logic, Construction, Computation, vol. 3 of Ontos-Verlag Mathematical Logic Series. De Gruyter, 2012, pp. 227–258.Google Scholar
  7. 7.
    Galatos, N., and H. Ono, Glivenko theorems for substructural logics over FL, Journal of Symbolic Logic 71:1353–1384, 2006.CrossRefGoogle Scholar
  8. 8.
    Glivenko, V., Sur quelques points de la logique de M. Brouwer, Bulletins de la Classe des Sciences 15(5):183–188, 1929.Google Scholar
  9. 9.
    Guerrieri, G., and A. Naibo, Postponement of raa and Glivenko’s Theorem, Revisited (long version), ArXiv e-prints,, 2017.
  10. 10.
    Kleene, S. C., Introduction to metamathematics, North-Holland, 1952.Google Scholar
  11. 11.
    Kuroda, S., Intuitionistische untersuchungen der formalistischen logik, Nagoya Mathematical Journal 2:35–47, 1951.CrossRefGoogle Scholar
  12. 12.
    Murthy, C., Extracting Constructive Content From Classical Proofs, Ph.D. thesis, Cornell University, 1990.Google Scholar
  13. 13.
    Nadathur, G., Uniform provability in classical logic, Journal of Logic and Computation 8(2):209–229, 1998.CrossRefGoogle Scholar
  14. 14.
    Ono, H., Glivenko theorems revisited, Annals of Pure and Applied Logic 161(2):246–250, 2009.CrossRefGoogle Scholar
  15. 15.
    Pereira, L. C., Translations and normalization procedures (abstract), in WoLLIC’2000—7th Workshop on Logic, Language, Information and Computation, pp. 21–24., 2000.
  16. 16.
    Pereira, L. C., and E. H. Haeusler, On constructive fragments of classical logic, in H. Wansing, (ed.), Dag Prawitz on Proofs and Meaning, vol. 7 of Outstanding Contributions to Logic, Springer, Berlin, 2015, pp. 281–292.Google Scholar
  17. 17.
    von Plato, J., Elements of Logical Reasoning, Cambridge University Press, 2013.Google Scholar
  18. 18.
    von Plato, J., and A. Siders, Normal derivability in classical natural deduction, The Review of Symbolic Logic 5:205–211, 2012.CrossRefGoogle Scholar
  19. 19.
    Prawitz, D., Natural Deduction: A proof-theoretical study, Almqvist & Wiksell, Stockholm, 1965.Google Scholar
  20. 20.
    Seldin, J. P., On the proof theory of the intermediate logic MH, The Journal of Symbolic Logic 51(3):626–647, 1986.CrossRefGoogle Scholar
  21. 21.
    Seldin, J. P., Normalization and excluded middle. I, Studia Logica 48(2):193–217, 1989.CrossRefGoogle Scholar
  22. 22.
    Stålmarck, G., Normalization theorems for full first order classical natural deduction, The Journal of Symbolic Logic 56(1):129–149 1991.CrossRefGoogle Scholar
  23. 23.
    Statman, R., Structural Complexity of Proofs, Ph.D. thesis, Stanford University, 1974.Google Scholar
  24. 24.
    Tennant, N., Anti-Realism and Logic: Truth as eternal, Oxford University Press, Oxford, 1987.Google Scholar
  25. 25.
    Zdanowski, K., On second order intuitionistic propositional logic without a universal quantifier, The Journal of Symbolic Logic 74(1):157–167, 2009.CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media B.V., part of Springer Nature 2018

Authors and Affiliations

  1. 1.Dipartimento di Informatica–Scienza e Ingegneria (DISI)Alma Mater Studiorum–Università di BolognaBolognaItaly
  2. 2.IHPST (UMR 8590)Université Paris 1 Panthéon–Sorbonne, CNRS, ENSParisFrance

Personalised recommendations