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.
Blok, W. J., and I. M. A. Ferreirim, On the structure of hoops, Algebra Universalis 43(2–3): 233–257, 2000.
Blok, W. J., and D. Pigozzi, On the structure of varieties with equationally definable principal congruences. III, Algebra Universalis 32(4): 545–608, 1994.
Blok, W. J., and J. G. Raftery, Varieties of commutative residuated integral pomonoids and their residuation subreducts, Journal of Algebra 190: 280–328, 1997.
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.
Büchi, J. R., and T. M. Owens, Complemented monoids and hoops, c. 1974. Unpublished manuscript.
Burris, S., and H. P. Sankappanavar, A Course in Universal Algebra, Springer, 1981. An updated version is available online via http://www.math.uwaterloo.ca/~snburris/.
Cignoli, R., and A. Torrens, Free algebras in varieties of BL-algebras with a Boolean retract, Algebra Universalis 48: 55–79, 2002.
Cignoli, R., and A. Torrens, Glivenko like theorems in natural expansions of bck-logic, Mathematical Logic Quarterly 50: 111–125, 2004.
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.
Farahani, H., and H. Ono, Glivenko theorems and negative translations in substructural predicate logics, Archive for Mathematical Logic 51: 695–707, 2012.
Ferreira, G., and P. Oliva, On the relation between various negative translations, Logic, Construction, Computation, Ontos-Verlag Mathematical Logic Series 3: 227–258, 2012.
Ferreirim, I. M. A., On Varieties and Quasivarieties of Hoops and their Reducts, Ph.D. thesis, University of Illinois at Chicago, 1992.
Font, J. M., A. J. Rodríguez, and A. Torrens, Wajsberg algebras, Stochastica 8: 5–31, 1984.
Galatos, N., and H. Ono, Glivenko theorems for substructural logics over FL, Journal of Symbolic Logic 71(4): 1353–1384, 2006.
Gentzen, G., Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik, galley proof (received in 1933), Mathematische Annalen, 1933.
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.
Gödel, K., Zum intuitionistischen Aussagenkalkül, Anzeiger der Akademie der Wissenschaften in Wien 69: 65–66, 1932.
Gödel, K., Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines Mathematischen Kolloquiums 4: 34–38, 1933.
Kolmogorov, A. N., On the principle of the excluded middle (Russian), Matematicheskii Sbornik 32: 646–667, 1925.
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.
Raftery, J. G., On the variety generated by involutive pocrims, Reports on Mathematical Logic 42: 71–86, 2007.
Troelstra, A. S., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, vol. 344, Springer, Berlin, 1973.
We thank: the late Franco Montagna for drawing our attention to  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.
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Presented by Hiroakira Ono
About this article
Cite this article
Arthan, R., Oliva, P. Double Negation Semantics for Generalisations of Heyting Algebras. Stud Logica 109, 341–365 (2021). https://doi.org/10.1007/s11225-020-09909-y
- Algebraic semantics
- Negative translation
- Double negation translation
- Involutive core
- Involutive replica