No CrossRef data available.
Article contents
CONSERVATION AS TRANSLATION
Published online by Cambridge University Press: 30 January 2025
Abstract
Glivenko’s theorem says that classical provability of a propositional formula entails intuitionistic provability of the double negation of that formula. This stood right at the beginning of the success story of negative translations, indeed mainly designed for converting classically derivable formulae into intuitionistically derivable ones. We now generalise this approach: simultaneously from double negation to an arbitrary nucleus; from provability in a calculus to an inductively generated abstract consequence relation; and from propositional logic to any set of objects whatsoever. In particular, we give sharp criteria for the generalisation of classical logic to be a conservative extension of the one of intuitionistic logic with double negation.
MSC classification
- Type
- Research Article
- Information
- Copyright
- © The Author(s), 2025. Published by Cambridge University Press on behalf of The Association for Symbolic Logic
Footnotes
This note grew out from a chapter of the first author’s doctoral thesis [33], and is a revised and extended version of a conference paper [35]. As compared to the latter, the main amendments include: the study of j-homogeneous functions and j-translations; a more informative statement of the Gödel conservation theorem; the new Kolmogorov conservation theorem and its corollary, the Kuroda conservation theorem; and an application to lax logic.
References
BIBLIOGRAPHY
Aczel, P. (1978). The type theoretic interpretation of constructive set theory. In Logic Colloquium ’77 (Proc. Conf., Wrocław, 1977), Studies in Logic and the Foundations of Mathematics, 96. Amsterdam: North-Holland, pp. 55–66.Google Scholar
Aczel, P. (1982). The type theoretic interpretation of constructive set theory: Choice principles. In The L. E. J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), Studies in Logic and the Foundations of Mathematics, 110. Amsterdam: North-Holland, pp. 1–40.Google Scholar
Aczel, P. (1986). The type theoretic interpretation of constructive set theory: inductive definitions. In Logic, Methodology and Philosophy of Science, VII (Salzburg, 1983), Studies in Logic and the Foundations of Mathematics, 114. Amsterdam: North-Holland, pp. 17–49.Google Scholar
Aczel, P. (2001). The Russell–Prawitz modality. Mathematical Structures in Computer Science, 11(4), 541–554.CrossRefGoogle Scholar
Aczel, P. (2006). Aspects of general topology in constructive set theory. Annals of Pure and Applied Logic, 137(1–3), 3–29.CrossRefGoogle Scholar
Aczel, P., & Rathjen, M. (2000). Notes on constructive set theory. Technical report, Institut Mittag-Leffler (The Royal Swedish Academy of Sciences), Report No. 40.Google Scholar
Aczel, P., & Rathjen, M. (2010). Constructive Set Theory. Book draft. https://ncatlab.org/nlab/files/AczelRathjenCST.pdf.Google Scholar
Bezhanishvili, G., & Holliday, W. H. (2019). A semantic hierarchy for intuitionistic logic. Indagationes Mathematicae, 30(3), 403–469.CrossRefGoogle Scholar
Béziau, J.-Y. (2006). Les axiomes de Tarski. In Pouivet, R., & Resbuschi, M., editors. La Philosophie en Pologne 1919–1939. Paris: Librairie Philosophique J. VRIN, pp. 135–149.Google Scholar
Birkhoff, G. (1948). Lattice Theory, American Mathematical Society Colloquium Publications, 25 (revised edition). New York: American Mathematical Society.Google Scholar
Bishop, E., & Bridges, D. (1987). Constructive analysis. Journal of Symbolic Logic, 52(4), 1047–1048.Google Scholar
Cederquist, J., & Coquand, T. (2000). Entailment relations and distributive lattices. In Buss, S. R., Hájek, P., & Pudlák, P., editors. Logic Colloquium ’98. Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Prague, Czech Republic, August 9–15, 1998. Lecture Notes in Logic, 13. Natick: A. K. Peters, pp. 127–139.Google Scholar
Cignoli, R., & Torrens, A. (2004). Glivenko like theorems in natural expansions of BCK-logic. Mathematical Logic Quarterly, 50, 111–125.CrossRefGoogle Scholar
Cintula, P., & Carles, N. (2013). The proof by cases property and its variants in structural consequence relations. Studia Logica, 101(4), 713–747.CrossRefGoogle Scholar
Ciraulo, F., Maietti, M. E., & Sambin, G. (2013). Convergence in formal topology: A unifying notion. Journal of Logic and Analysis, 5(2), 1–45.CrossRefGoogle Scholar
Ciraulo, F., & Sambin, G. (2008). Finitary formal topologies and Stone’s representation theorem. Theoretical Computer Science, 405(1–2), 11–23.CrossRefGoogle Scholar
Coquand, T. (2000). A Direct Proof of the Localic Hahn–Banach Theorem. Available from: https://ncatlab.org/nlab/files/AczelRathjenCST.pdf.Google Scholar
Coquand, T. (2000). Lewis Carroll, Gentzen and Entailment Relations. Available from: https://ncatlab.org/nlab/files/AczelRathjenCST.pdf.Google Scholar
Coquand, T. (2005). About Stone’s notion of spectrum. Journal of Pure and Applied Algebra, 197(1–3), 141–158.CrossRefGoogle Scholar
Coquand, T. (2009). Space of valuations. Annals of Pure and Applied Logic, 157, 97–109.CrossRefGoogle Scholar
Coquand, T., & Lombardi, H. (2002). Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative rings. In Fontana, M., Kabbaj, S.-E., & Wiegand, S., editors. Commutative Ring Theory and Applications, Lecture Notes in Pure and Applied Mathematics, 231. Reading, MA: Addison-Wesley, pp. 477–499.Google Scholar
Coquand, T., Lombardi, H., & Neuwirth, S. (2019). Lattice-ordered groups generated by an ordered group and regular systems of ideals. The Rocky Mountain Journal of Mathematics, 49(5), 1449–1489.CrossRefGoogle Scholar
Coquand, T., & Neuwirth, S. (2017). An introduction to Lorenzen’s “algebraic and logistic investigations on free lattices” (1951). Preprint.Google Scholar
Coquand, T., & Persson, H. (2001). Valuations and Dedekind’s Prague theorem. Journal of Pure and Applied Algebra, 155(2–3), 121–129.CrossRefGoogle Scholar
Coquand, T., & Zhang, G.-Q. (2000). Sequents, frames, and completeness. In Clote, P. G., & Schwichtenberg, H., editors. Computer Science Logic (Fischbachau, 2000), Lecture Notes in Computer Science, 1862. Berlin: Springer, pp. 277–291.CrossRefGoogle Scholar
Escardó, M., & Oliva, P. (2010). The Peirce translation and the double negation shift. In Ferreira, F., Löwe, B., Mayordomo, E., & Gomes, L. M., editors. Programs, Proofs, Processes. Berlin, Heidelberg: Springer, pp. 151–161.CrossRefGoogle Scholar
Escardó, M., & Oliva, P. (2012). The Peirce translation. Annals of Pure and Applied Logic, 163, 681–692.CrossRefGoogle Scholar
Espíndola, C. (2013). A short proof of Glivenko theorems for intermediate predicate logics. Archive for Mathematical Logic, 52(7–8), 823–826.CrossRefGoogle Scholar
Fairtlough, M., & Mendler, M. (1997). Propositional lax logic. Information and Computation, 137(1), 1–33.CrossRefGoogle Scholar
Fellin, G. (2022). Constructivisation through Induction and Conservation. Ph.D. Thesis, University of Helsinki & University of Trento, Unigrafia, Helsinki.Google Scholar
Fellin, G., Negri, S., & Orlandelli, E. (2023). Glivenko sequent classes and constructive cut elimination in geometric logics. Archive for Mathematical Logic, 62, 657–688.CrossRefGoogle Scholar
Fellin, G., & Schuster, P. (2021). A general Glivenko–Gödel theorem for nuclei. In Sokolova, A., editor. Proceedings of the 37th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2021, Salzburg, Austria, August 29–September 3, 2021, Electronic Notes in Theoretical Computer Science. Amsterdam: Elsevier, pp. 51–66.Google Scholar
Fellin, G., Schuster, P., & Wessel, D. (2022). The Jacobson radical of a propositional theory. Bulletin of Symbolic Logic, 28(2), 163–181.CrossRefGoogle Scholar
Ferreira, G., & Oliva, P. (2013). On the relation between various negative translations. In Berger, U., Diener, H., Schuster, P., & Seisenberger, M., editors. Logic, Construction, Computation. Frankfurt: De Gruyter, pp. 227–258.Google Scholar
Friedman, H. (1978). Classically and intuitionistically provably recursive functions. In Müller, G. H., & Scott, D. S., editors. Higher Set Theory (Proc. Conf., Math. Forschungsinst., Oberwolfach, 1977). Lecture Notes in Mathematics, 669. Berlin: Springer, pp. 21–27.Google Scholar
Gabbay, D. M. (1972). Applications of trees to intermediate logics. Journal of Symbolic Logic, 37(1), 135–138.CrossRefGoogle Scholar
Galatos, N., & Ono, H. (2006). Glivenko theorems for substructural logics over FL. The Journal of Symbolic Logic, 71(4), 1353–1384.CrossRefGoogle Scholar
Gentzen, G. (1936). Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112(1), 493–565.CrossRefGoogle Scholar
Gentzen, G. (1938). Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, 4, 19–44.Google Scholar
Gentzen, G. (1974). Über das Verhä ltnis zwischen intuitionistischer und klassischer Arithmetik. Archiv für mathematische Logik und Grundlagenforschung, 16, 119–132.CrossRefGoogle Scholar
Glivenko, V. (1928). Sur la logique de M. Brouwer. Académie Royale de Belgique, Bulletins de la classe des sciences (5), 14, 225–228.Google Scholar
Glivenko, V. (1929). Sur quelques points de la Logique de M. Brouwer. Académie Royale de Belgique, Bulletins de la classe des sciences (5), 15, 183–188.Google Scholar
Gödel, K. (1933). Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines math. Kolloquiums, 4, 39–40.Google Scholar
Gödel, K. (1986). Zur intuitionistischen Arithmetik und Zahlentheorie (gekuerzter Nachdruck). In Berka, K., & Kreiser, L., editors. Logik-Texte: Kommentierte Auswahl Zur Geschichte der Modernen Logik (Vierte Auflage). Berlin: Akademie-Verlag, pp. 201–202.Google Scholar
Griffin, T. (1990). A formulae-as-types notion of control. In Allen, F. E., editor. Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990. New York: ACM Press, pp. 47–58. https://doi.org/10.1145/96709.96714.CrossRefGoogle Scholar
Guerrieri, G., & Naibo, A. (2019). Postponement of
$\mathsf{raa}$
and Glivenko’s theorem, revisited. Studia Logica, 107(1), 109–144.CrossRefGoogle Scholar
$\mathsf{raa}$
and Glivenko’s theorem, revisited. Studia Logica, 107(1), 109–144.CrossRefGoogle ScholarHaykazyan, L. (2020). More on a curious nucleus. Journal of Pure and Applied Algebra, 224, 860–868.CrossRefGoogle Scholar
Hertz, P. (1922). Über Axiomensysteme für beliebige Satzsysteme. I. Teil. Sätze ersten grades. Mathematische Annalen, 87(3), 246–269.CrossRefGoogle Scholar
Hertz, P. (1923). Über Axiomensysteme für beliebige Satzsysteme. II. Teil. Sätze höheren grades. Mathematische Annalen, 89(1), 76–102.CrossRefGoogle Scholar
Hertz, P. (1929). Über Axiomensysteme für beliebige Satzsysteme. Mathematische Annalen, 101(1), 457–514.CrossRefGoogle Scholar
Ilik, D. (2013). Double-negation shift as a constructive principle. CoRR, Preprint, abs/1301.5089.Google Scholar
Ishihara, H. (2000). A note on the Gödel–Gentzen translation. Mathematical Logic Quarterly, 46, 135–137.3.0.CO;2-R>CrossRefGoogle Scholar
Ishihara, H., & Nemoto, T. (2016). A note on the independence of premiss rule. Mathematical Logic Quarterly, 62(1–2), 72–76.CrossRefGoogle Scholar
Ishihara, H., & Schwichtenberg, H. (2016). Embedding classical in minimal implicational logic. Mathematical Logic Quarterly, 62(1–2), 94–101.CrossRefGoogle Scholar
Jibladze, M., & Johnstone, P. T. (1991). The frame of fibrewise closed nuclei. Cahiers de Topologie et Geometrie Differentielle Categoriques, 32, 99–112.Google Scholar
Johansson, I. (1937). Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus. Compositio Mathematica, 4, 119–136.Google Scholar
Johnstone, P. T. (1982). Stone Spaces, Cambridge Studies in Advanced Mathematics, 3. Cambridge: Cambridge University Press.Google Scholar
Johnstone, P. T. (1991). The art of pointless thinking: a student’s guide to the category of locales. In Herrlich, H., & Porst, H.-E., editors. Category Theory at Work. Berlin: Heldermann Verlag, pp. 85–107.Google Scholar
Johnstone, P. T. (2002). Sketches of an Elephant: A Topos Theory Compendium, Vol. 1 & 2. New York: Oxford University Press.Google Scholar
Kohlenbach, U. (2008). Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Monographs in Mathematics. Berlin: Springer-Verlag.Google Scholar
Kolmogorov, A. N. (1925). On the principle of the excluded middle (Russian). Matematicheskii Sbornik, 32, 646–667.Google Scholar
Krivine, J.-L. (1990). Opérateurs de mise en mémoire et traduction de Gödel. Archive for Mathematical Logic, 30(4), 241–267.CrossRefGoogle Scholar
Kuroda, S. (1951). Intuitionistische Untersuchungen der formalistischen Logik. Nagoya Mathematical Journal, 3, 35–47.CrossRefGoogle Scholar
Legris, J. (2012). Paul Hertz and the origins of structural reasoning. In Béziau, J.-Y., editor. Universal Logic: An Anthology. From Paul Hertz to Dov Gabbay, Studies in Universal Logic. Basel: Birkhäuser, pp. 3–10.CrossRefGoogle Scholar
Litak, T., Polzer, M., & Rabenstein, U. (2017). Negative translations and normal modality. In 2nd International Conference on Formal Structures for Computation and Deduction, LIPIcs, Leibniz International Proceedings in Informatics, 84. Article no. 27, 18. Wadern: Schloss Dagstuhl. Leibniz-Zent. Inform.Google Scholar
Lombardi, H., & Quitté, C. (2015). Commutative Algebra: Constructive Methods. Finite Projective Modules, Algebra and Applications, 20. Dordrecht: Springer.CrossRefGoogle Scholar
Macnab, D. S. (1981). Modal operators on heyting algebras. Algebra Universalis, 12, 5–29.CrossRefGoogle Scholar
Mines, R., Richman, F., & Ruitenburg, W. (1988). A Course in Constructive Algebra. New York: Springer.CrossRefGoogle Scholar
Miquel, A. (2020). Implicative algebras: A new foundation for realizability and forcing. Mathematical Structures in Computer Science, 30(5), 458–510.CrossRefGoogle Scholar
Murthy, C. R. (1990). Extracting Constructive Content from Classical Proofs. Ph.D. Thesis, Cornell University.Google Scholar
Nadathur, G. (2000). Correspondences between classical, intuitionistic and uniform provability. Theoretical Computer Science, 232, 273–298.CrossRefGoogle Scholar
Negri, S. (1996). Stone bases alias the constructive content of stone representation. In Ursini, A., & Aglianò, P., editors. Logic and Algebra. Proceedings of the International Conference Dedicated to the Memory of Roberto Magari, April 26–30, 1994, Pontignano, Italy, Lecture Notes in Pure and Applied Mathematics, 180. New York: Marcel Dekker, pp. 617–636.Google Scholar
Negri, S. (2002). Continuous domains as formal spaces. Mathematical Structures in Computer Science, 12(1), 19–52.CrossRefGoogle Scholar
Negri, S. (2003). Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem. Archive for Mathematical Logic, 42(4), 389–401.CrossRefGoogle Scholar
Negri, S. (2016). Glivenko sequent classes in the light of structural proof theory. Archive for Mathematical Logic, 55(3–4), 461–473.CrossRefGoogle Scholar
Negri, S. (2021). Geometric rules in infinitary logic. In Arieli, O., & Zamansky, A., editors. Arnon Avron on Semantics and Proof Theory of Non-Classical Logics. Cham: Springer, pp. 265–293.CrossRefGoogle Scholar
Negri, S., von Plato, J., & Coquand, T. (2004). Proof-theoretical analysis of order relations. Archive for Mathematical Logic, 43, 297–309.CrossRefGoogle Scholar
Odintsov, S. (2008). Constructive Negations and Paraconsistency. Dordrecht: Springer.CrossRefGoogle Scholar
Odintsov, S. P. (2004). Negative equivalence of extensions of minimal logic. Studia Logica, 78(3), 417–442.CrossRefGoogle Scholar
Ono, H. (2009). Glivenko theorems revisited. Annals of Pure and Applied Logic, 161(2), 246–250.CrossRefGoogle Scholar
Orevkov, V. P. (1968). Glivenko’s sequence classes. In Orevkov, V. P., editor. Logical and Logico-mathematical Calculi. Part 1. Providence: American Mathematical Society, pp. 131–154.Google Scholar
Pereira, L. C., & Haeusler, E. H. (2015). On constructive fragments of classical logic. In Wansing, H., editor. Dag Prawitz on Proofs and Meaning, Outstanding Contributions to Logic, 7. Cham: Springer, pp. 281–292.CrossRefGoogle Scholar
Picado, J., & Pultr, A. (2012). Frames and Locales. Topology without Points, Frontiers in Mathematics. Basel: Birkhäuser.CrossRefGoogle Scholar
Restall, G. (2000). An Introduction to Substructural Logics. London: Routledge.CrossRefGoogle Scholar
Rinaldi, D. (2014). Formal Methods in the Theories of Rings and Domains. Doctoral dissertation, Universität München.Google Scholar
Rinaldi, D., Schuster, P., & Wessel, D. (2017). Eliminating disjunctions by disjunction elimination. Bulletin of Symbolic Logic, 23(2), 181–200.CrossRefGoogle Scholar
Rinaldi, D., Schuster, P., & Wessel, D. (2018). Eliminating disjunctions by disjunction elimination. Indagationes Mathematicae (N.S.), 29(1), 226–259. Communicated first in Bulletin of Symbolic Logic, 23(2017), 181–200.CrossRefGoogle Scholar
Rinaldi, D., & Wessel, D. (2018). Extension by conservation. Sikorski’s theorem. Logical Methods in Computer Science, 14(4–8), 1–17.Google Scholar
Rinaldi, D., & Wessel, D. (2019). Cut elimination for entailment relations. Archive for Mathematical Logic, 58(5–6), 605–625.CrossRefGoogle Scholar
Rosenthal, K. I. (1990). Quantales and Their Applications, Pitman Research Notes in Mathematics, 234. Essex: Longman Scientific & Technical.Google Scholar
Rump, W. (2009). A general Glivenko theorem. Algebra Universalis, 61, 455–473.CrossRefGoogle Scholar
Sambin, G. (1987). Intuitionistic formal spaces—A first communication. In Skordev, D., editor. Mathematical Logic and its Applications, Proc. Adv. Internat. Summer School Conf., Druzhba, Bulgaria, 1986. New York: Plenum, pp. 187–204.Google Scholar
Sambin, G. (2003). Some points in formal topology. Theoretical Computer Science, 305(1–3), 347–408.CrossRefGoogle Scholar
Sambin, G. (forthcoming). The Basic Picture. Structures for Constructive Topology, Oxford Logic Guides. Oxford: Clarendon Press. Available from: https://www.math.unipd.it/~sambin/txt/BPbookContentsOct2006.pdf.Google Scholar
Schlagbauer, K., Schuster, P., & Wessel, D. (2019). Der Satz von Hahn–Banach per Disjunktionselimination. Confluentes Mathematici, 11(1), 79–93.CrossRefGoogle Scholar
Schuster, P., & Wessel, D. (2020). Resolving finite indeterminacy: A definitive constructive universal prime ideal theorem. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’20. New York: Association for Computing Machinery, pp. 820–830.CrossRefGoogle Scholar
Schwichtenberg, H., & Senjak, C. (2013). Minimal from classical proofs. Annals of Pure and Applied Logic, 164(6), 740–748.CrossRefGoogle Scholar
Schwichtenberg, H., & Wainer, S. S. (2012). Proofs and Computations, Perspectives in Logic. Cambridge: Cambridge University Press.Google Scholar
Scott, D. (1971). On engendering an illusion of understanding. Journal of Philosophy, 68, 787–807.CrossRefGoogle Scholar
Scott, D. (1974). Completeness and axiomatizability in many-valued logic. In Henkin, L., Addison, J., Chang, C. C., Craig, W., Scott, D., & Vaught, R., editors. Proceedings of the Tarski Symposium (Proc. Sympos. Pure Math., Vol. XXV, University of California, Berkeley, CA, 1971). Providence: American Mathematical Society, pp. 411–435.Google Scholar
Scott, D. S. (1973). Background to formalization. In Leblanc, H., editor. Truth, Syntax and Modality (Proc. Conf. Alternative Semantics, Temple Univ., Philadelphia, PA, 1970), Studies in Logic and the Foundations of Mathematics, 68. Amsterdam: North-Holland, pp. 244–273.Google Scholar
Simmons, H. (1978). A framework for topology. In Macintyre, A., Pacholski, L., & Paris, J., editors. Logic Colloquium ’77, Studies in Logic and the Foundations of Mathematics, 96. Amsterdam: North-Holland, pp. 239–251.CrossRefGoogle Scholar
Simmons, H. (2010). A curious nucleus. Journal of Pure and Applied Algebra, 214, 2063–2073.CrossRefGoogle Scholar
Spector, C. (1962). Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In Recursive Function Theory: Proceedings of Symposia in Pure Mathematics, Vol. 5. Providence: American Mathematical Society, pp. 1–27.CrossRefGoogle Scholar
Streicher, T., & Reus, B. (1998). Classical logic, continuation semantics and abstract machines. Journal of Functional Programming, 8(6), 543–572.CrossRefGoogle Scholar
Tarski, A. (1930). Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften. I. Monatshefte für Mathematik, 37, 361–404.CrossRefGoogle Scholar
Torrens, A. (2008). An approach to Glivenko’s theorem in algebraizable logics. Studia Logica, 88, 349–383.CrossRefGoogle Scholar
Troelstra, A. S., & van Dalen, D. (1988). Constructivism in Mathematics: An Introduction, Studies in Logic and the Foundations of Mathematics, II. Amsterdam: North-Holland.Google Scholar
van den Berg, B. (2019). A Kuroda-style
$j$
-translation. Archive for Mathematical Logic, 58(5), 627–634.CrossRefGoogle Scholar
$j$
-translation. Archive for Mathematical Logic, 58(5), 627–634.CrossRefGoogle Scholarvan den Berg, B. (2022). Implicative algebras for modified realizability. Conference presentation abstract, Continuity, Computability, Constructivity. From Logic to Algorithms, Padua, Italy: Università degli Studi di Padova. Available from: https://events.math.unipd.it/ccc2022/submissions/CCC2022_paper_2336.pdf.Google Scholar
Wang, S.-m., & Cintula, P. (2008). Logics with disjunction and proof by cases. Archive for Mathematical Logic, 47(5), 435–446.CrossRefGoogle Scholar
Wessel, D. (2019). Ordering groups constructively. Communications in Algebra, 47(12), 4853–4873.CrossRefGoogle Scholar
Wessel, D. (2019). Point-free spectra of linear spreads. In Centrone, S., Negri, S., Sarikaya, D., & Schuster, P., editors. Mathesis Universalis, Computability and Proof, Synthese Library. Cham: Springer, pp. 353–374.CrossRefGoogle Scholar
Zdanowski, K. (2009). On second order intuitionistic propositional logic without a universal quantifier. Journal of Symbolic Logic, 74, 157–167.CrossRefGoogle Scholar