Double Negation Semantics for Generalisations of Heyting Algebras


This paper presents an algebraic framework for investigating proposed translations of classical logic into intuitionistic logic, such as the four negative translations introduced by Kolmogorov, Gödel, Gentzen and Glivenko. We view these as variant semantics and present a semantic formulation of Troelstra’s syntactic criteria for a satisfactory negative translation. We consider how each of the above-mentioned translation schemes behaves on two generalisations of Heyting algebras: bounded pocrims and bounded hoops. When a translation fails for a particular class of algebras, we demonstrate that failure via specific finite examples. Using these, we prove that the syntactic version of these translations will fail to satisfy Troelstra’s criteria in the corresponding substructural logical setting.


  1. 1.

    Blok, W. J., and I. M. A. Ferreirim, On the structure of hoops, Algebra Universalis 43(2–3): 233–257, 2000.

    Article  Google Scholar 

  2. 2.

    Blok, W. J., and D. Pigozzi, On the structure of varieties with equationally definable principal congruences. III, Algebra Universalis 32(4): 545–608, 1994.

    Article  Google Scholar 

  3. 3.

    Blok, W. J., and J. G. Raftery, Varieties of commutative residuated integral pomonoids and their residuation subreducts, Journal of Algebra 190: 280–328, 1997.

    Article  Google Scholar 

  4. 4.

    Bova, S., and F. Montagna, The consequence relation in the logic of commutative GBL-algebras is PSPACE-complete, Theoretical Computer Science 410(12–13): 1143–1158, 2009.

    Article  Google Scholar 

  5. 5.

    Büchi, J. R., and T. M. Owens, Complemented monoids and hoops, c. 1974. Unpublished manuscript.

  6. 6.

    Burris, S., and H. P. Sankappanavar, A Course in Universal Algebra, Springer, 1981. An updated version is available online via

  7. 7.

    Cignoli, R., and A. Torrens, Free algebras in varieties of BL-algebras with a Boolean retract, Algebra Universalis 48: 55–79, 2002.

    Article  Google Scholar 

  8. 8.

    Cignoli, R., and A. Torrens, Glivenko like theorems in natural expansions of bck-logic, Mathematical Logic Quarterly 50: 111–125, 2004.

    Article  Google Scholar 

  9. 9.

    Escardó, M. H., and P. Oliva, The Peirce translation and the double negation shift, in F. Ferreira, B. Löwe, E. Mayordomo, and L. M. Gomes, (eds.), Programs, Proofs, Processes—CiE 2010, LNCS 6158, Springer, 2010, pp. 151–161.

  10. 10.

    Farahani, H., and H. Ono, Glivenko theorems and negative translations in substructural predicate logics, Archive for Mathematical Logic 51: 695–707, 2012.

    Article  Google Scholar 

  11. 11.

    Ferreira, G., and P. Oliva, On the relation between various negative translations, Logic, Construction, Computation, Ontos-Verlag Mathematical Logic Series 3: 227–258, 2012.

    Google Scholar 

  12. 12.

    Ferreirim, I. M. A., On Varieties and Quasivarieties of Hoops and their Reducts, Ph.D. thesis, University of Illinois at Chicago, 1992.

  13. 13.

    Font, J. M., A. J. Rodríguez, and A. Torrens, Wajsberg algebras, Stochastica 8: 5–31, 1984.

    Google Scholar 

  14. 14.

    Galatos, N., and H. Ono, Glivenko theorems for substructural logics over FL, Journal of Symbolic Logic 71(4): 1353–1384, 2006.

    Article  Google Scholar 

  15. 15.

    Gentzen, G., Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik, galley proof (received in 1933), Mathematische Annalen, 1933.

  16. 16.

    Glivenko, V. I., Sur quelques points de la logique de M. Brouwer, Bulletin de la Société Mathématique de Belgique 15: 183–188, 1929.

    Google Scholar 

  17. 17.

    Gödel, K., Zum intuitionistischen Aussagenkalkül, Anzeiger der Akademie der Wissenschaften in Wien 69: 65–66, 1932.

    Google Scholar 

  18. 18.

    Gödel, K., Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines Mathematischen Kolloquiums 4: 34–38, 1933.

    Google Scholar 

  19. 19.

    Kolmogorov, A. N., On the principle of the excluded middle (Russian), Matematicheskii Sbornik 32: 646–667, 1925.

    Google Scholar 

  20. 20.

    Ono, H., Glivenko theorems revisited, Annals of Pure and Applied Logic 161(2): 246–250, 2009. Festschrift on the occasion of Franco Montagna’s 60th birthday.

  21. 21.

    Raftery, J. G., On the variety generated by involutive pocrims, Reports on Mathematical Logic 42: 71–86, 2007.

    Google Scholar 

  22. 22.

    Troelstra, A. S., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, vol. 344, Springer, Berlin, 1973.

Download references


We thank: the late Franco Montagna for drawing our attention to [4] and for a manuscript proof that the equational theory of commutative GBL-algebras is a conservative extension of that of hoops; George Metcalfe for encouraging remarks and for pointers to the literature; and Isabel Ferreirim for helpful correspondence about the theory of hoops. Particular thanks are due to the anonymous referees for their careful reading of our draft and for their insightful and constructive comments.

Author information



Corresponding author

Correspondence to Paulo Oliva.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Presented by Hiroakira Ono

Rights and permissions

Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Arthan, R., Oliva, P. Double Negation Semantics for Generalisations of Heyting Algebras. Stud Logica 109, 341–365 (2021).

Download citation


  • Pocrims
  • Hoops
  • Algebraic semantics
  • Negative translation
  • Double negation translation
  • Involutive core
  • Involutive replica