Document Open Access Logo

A Unifying Conservation Theorem

Author Giulio Fellin

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.19.pdf
  • Filesize: 0.82 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • double negation
  • negative translation
  • conservation
  • minimal logic
  • Glivenko’s theorem

Metrics

Abstract

The relationship between classical and constructive logics has long been illuminated by a series of conservation results, beginning with Kolmogorov’s negative translation and Glivenko’s double negation theorem, and later extended by Kuroda and Segerberg to first-order and minimal logics respectively. These results reveal how certain classical principles can be interpreted or recovered within weaker constructive frameworks, either via translations or through minimal extensions that satisfy specific logical properties. In this paper, we propose a unifying generalisation of these conservation theorems, that consolidates and expands the abstract methods introduced in earlier studies, offering a unified perspective on the interplay between classical provability and constructive reasoning.

Cite As Get BibTex

Giulio Fellin. A Unifying Conservation Theorem. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.19

Author Details

Giulio Fellin
  • Università degli Studi di Verona, Italy

Acknowledgements

The author wishes to thank Thorsten Altenkirch, Norbert Gratzl, Edi Pavlović, and Peter Schuster for their interest and valuable suggestions. The author is a member of the "Gruppo Nazionale per le Strutture Algebriche, Geometriche e le loro Applicazioni" (GNSAGA) of the Istituto Nazionale di Alta Matematica (INdAM).

References

  1. Peter Aczel. The Russell–Prawitz modality. Mathematical Structures in Computer Science, 11:541-554, 2001. URL: https://doi.org/10.1017/S0960129501003309.
  2. Peter Aczel. Aspects of general topology in constructive set theory. Annals of Pure and Applied Logic, 137:3-29, 2006. URL: https://doi.org/10.1016/j.apal.2005.05.016.
  3. Giacomo Bartoli, Giulio Fellin, and Matteo Tesi. Infinitary negative translations and Glivenko logic. Submitted, 2025. Google Scholar
  4. Marcel Barzin and Alfred Errera. Sur la logique de M. Brouwer. Bulletin de la Classe des Sciences. Académie royale de Belgique, 13:56-71, 1927. URL: https://dipot.ulb.ac.be/dspace/bitstream/2013/233730/4/ce95c10e-1981-4536-8077-6e2caefcaf78.txt.
  5. L. E. J. Brouwer. Over de Grondslagen der Wiskunde. Universiteit van Amsterdam, 1907. Ph.D. thesis. URL: https://eprints.illc.uva.nl/id/eprint/1852/2/HDS-20-LEJBrouwer.text.pdf.
  6. L. E. J. Brouwer. De onbetrouwbaarheid der logische principes. Noordhoff, Groningen, 1908. Google Scholar
  7. René David, Karim Nour, and Christophe Raffali. Introduction à la Logique. Théorie de la démonstration. Dunod, 2004. Google Scholar
  8. Martín Hötzel Escardó and Paulo Oliva. The Peirce translation. Annals of Pure and Applied Logic, 163(6):681-692, 2012. URL: https://doi.org/10.1016/J.APAL.2011.11.002.
  9. Giulio Fellin, Sara Negri, and Eugenio Orlandelli. Glivenko sequent classes and constructive cut elimination in geometric logics. Archive for Mathematical Logic, 62(5-6):657-688, 2023. URL: https://doi.org/10.1007/S00153-022-00857-Z.
  10. Giulio Fellin, Sara Negri, and Peter Schuster. Nuclear shifts for conservation. Unpublished preprint, 2025. Google Scholar
  11. Giulio Fellin and Peter Schuster. Conservation as translation. Review of Symbolic Logic, 18(1):316-348, 2025. URL: https://doi.org/10.1017/S1755020324000170.
  12. Giulio Fellin, Peter Schuster, and Daniel Misselbeck-Wessel. The Jacobson radical of a propositional theory. Bulletin of Symbolic Logic, 28(2):163-181, 2022. URL: https://doi.org/10.1017/BSL.2021.66.
  13. Giulio Fellin and Peter M. Schuster. A general Glivenko-Gödel theorem for nuclei. In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of EPTCS, pages 51-66, 2021. URL: https://doi.org/10.4204/EPTCS.351.4.
  14. Giulio Fellin, Tarmo Uustalu, and Cheng-Syuan Wan. Glivenko’s theorem beyond structure. Submitted, 2025. Google Scholar
  15. Gilda Ferreira and Paulo Oliva. On the relation between various negative trans- lations. In Ulrich Berger, Hannes Diener, Peter Schuster, and Monika Seisenberger, editors, Logic, Construction, Computation, pages 227-258, Frankfurt, 2013. De Gruyter. URL: https://doi.org/10.1515/9783110324921.227.
  16. Gerhard Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112:493-565, 1936. URL: https://doi.org/10.1007/BF01565428.
  17. Valery Glivenko. Sur la logique de M. Brouwer. Académie royale de Belgique. Bulletin de la Classe des Sciences, 14(5):225-228, 1928. URL: https://upload.wikimedia.org/wikipedia/commons/0/07/Sur_la_logique_de_M_Brouwer.pdf.
  18. Valery Glivenko. Sur quelques points de la logique de M. Brouwer. Académie royale de Belgique. Bulletin de la Classe des Sciences, 15(5):183-188, 1929. URL: https://upload.wikimedia.org/wikipedia/commons/5/5b/Sur_quelque_points_de_la_logique_de_M_Brouwer.pdf.
  19. Kurt Gödel. Zur intuitionistischen Arithmetik und Zahlentheorie (1933e). In Solomon Feferman, John W. Dawson Jr., Stephen C. Kleene, Gregory H. Moore, Robert M. Solovay, and Jean van Heijenoort, editors, Collected Works, Volume I: Publications 1929-1936, pages 286-294. Clarendon Press / Oxford University Press, New York and Oxford, 1986. Includes English translation On intuitionistic arithmetic and number theory (pp. 287-295) and A. S. Troelstra’s introductory note (pp. 282-287). URL: https://doi.org/10.1093/oso/9780195147209.003.0063.
  20. Robert Ian Goldblatt. Decidability of some extensions of J. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 20:203-205, 1974. URL: https://doi.org/10.1002/malq.19740201304.
  21. Timothy G. Griffin. A formulae-as-types notion of control. In Proceedings of the Principles of Programming Languages (POPL '90), pages 47-58, New York, NY, USA, 1989. Association for Computing Machinery. URL: https://doi.org/10.1145/96709.96714.
  22. Levon Haykazyan. More on a curious nucleus. Journal of Pure and Applied Algebra, 224:860-868, 2020. URL: https://doi.org/10.1016/j.jpaa.2019.06.014.
  23. Arend Heyting. Die formalen Regeln der intuitionistischen Logik I. Sitzungsberichte der Preussischen Akademie der Wissenschaften, pages 42-56, 1930. Google Scholar
  24. Ingebrigt Johansson. Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus. Compositio Mathematica, 4:119-136, 1937. URL: http://eudml.org/doc/88648.
  25. Peter T. Johnstone. Stone Spaces, volume 3 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982. Google Scholar
  26. Ulrich Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg, 2008. URL: https://doi.org/10.1007/978-3-540-77533-1.
  27. Andrey N. Kolmogoroff. Sur le principe de tertium non datur. Matematicheskii Sbornik, 32(4):646-667, 1925. Zbl: https://zbmath.org/?q=an:51.0048.01. URL: http://mi.mathnet.ru/sm7425.
  28. Sigekatu Kuroda. Intuitionistische Untersuchungen der formalistischen Logik. Nagoya Mathematical Journal, 3:35-47, 1951. URL: https://doi.org/10.1017/S0027763000010023.
  29. Chetan R. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, 1990. URL: https://ecommons.cornell.edu/items/2f12c8d8-71fd-4dbc-80ae-7b5948faaae8.
  30. Sara Negri. Continuous domains as formal spaces. Mathematical Structures in Computer Science, 12:19-52, 2002. URL: https://doi.org/10.1017/S0960129501003450.
  31. Sara Negri. Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem. Archive for Mathematical Logic, 42(4):389-401, 2003. URL: https://doi.org/10.1007/s001530100124.
  32. Sara Negri. Glivenko sequent classes in the light of structural proof theory. Archive for Mathematical Logic, 55(3-4):461-473, 2016. URL: https://doi.org/10.1007/s00153-016-0474-y.
  33. Sara Negri. Geometric rules in infinitary logic. In Ofer Arieli and Anna Zamansky, editors, Arnon Avron on Semantics and Proof Theory of Non-Classical Logics, pages 265-293. Springer, Cham, 2021. URL: https://doi.org/10.1007/978-3-030-71258-7_12.
  34. Sara Negri and Jan von Plato. Structural Proof Theory. Cambridge University Press, Cambridge, 2001. URL: https://doi.org/10.1017/CBO9780511527340.
  35. Sergei P. Odintsov. Logic of classical refutability and extensions of minimal logic. Logic and Logical Philosophy, 9:91-107, 2004. URL: https://doi.org/10.12775/LLP.2001.006.
  36. Vladimir P. Orevkov. On Glivenko sequent classes. Proceedings of the Steklov Institute of Mathematics, 98:147-173, 1968. Translated from the Russian original: "O glivenkovskikh klassakh sekventsii" (On Glivenko’s sequent classes), in Logical and Logical-Mathematical Calculus. Part I, Trudy Matematicheskogo Instituta Imeni V. A. Steklova, 98 (1968), 131-154. URL: http://mi.mathnet.ru/tm2930.
  37. Fred Richman. Confessions of a formalist, platonist, intuitionist. Unpublished manuscript, April 9, 1994. Formerly available at Richman’s personal website (no longer accessible). Google Scholar
  38. Fred Richman. Intuitionism as generalization. Philosophia Mathematica, 5(1-2):124-128, 1990. URL: https://doi.org/10.1093/philmat/s2-5.1-2.124.
  39. Kimmo I. Rosenthal. Quantales and their Applications, volume 234 of Pitman Research Notes in Mathematics. Longman Scientific & Technical, Essex, 1990. Google Scholar
  40. Helmut Schwichtenberg and Stanley S. Wainer. Proofs and Computations. Perspectives in Logic. Cambridge University Press and Association for Symbolic Logic, 2012. URL: https://doi.org/10.1017/CBO9781139031905.
  41. Krister Segerberg. Propositional logics related to Heyting’s and Johansson’s. Theoria, 34(1):26-61, 1968. URL: https://doi.org/10.1111/j.1755-2567.1968.tb00337.x.
  42. Harold Simmons. A framework for topology. In Angus Macintyre, Leszek Pacholski, and Jeff Paris, editors, Logic Colloquium '77, volume 96 of Studies in Logic and the Foundations of Mathematics, pages 239-251. Elsevier, 1978. URL: https://doi.org/10.1016/S0049-237X(08)72007-X.
  43. Harold Simmons. A curious nucleus. Journal of Pure and Applied Algebra, 214:2063-2073, 2010. URL: https://doi.org/10.1016/j.jpaa.2010.02.011.
  44. Clifford Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In Jacob C. E. Dekker, editor, Recursive Function Theory, volume 5 of Proceedings of Symposia in Pure Mathematics, pages 1-27. American Mathematical Society, Providence, RI, 1962. Google Scholar
  45. Christian Thiel. Die kontroverse um die intuitionistische logik vor ihrer axiomatisierung durch heyting im jahre 1930. History and Philosophy of Logic, 9(1):67-75, 1988. URL: https://doi.org/10.1080/01445348808837126.
  46. Anne S. Troelstra and Helmut Schwichtenberg. Basic Proof Theory. Cambridge University Press, Cambridge, 2nd edition, 2000. Google Scholar
  47. Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics: An Introduction, volume I and II. North-Holland, Amsterdam, 1988. Google Scholar
  48. Benno van den Berg. A Kuroda-style j-translation. Archive for Mathematical Logic, 58:627-634, 2019. URL: https://doi.org/10.1007/s00153-018-0656-x.
  49. Peter W. Woodruff. A note on JP'. Theoria, 36:183-184, 1970. URL: https://doi.org/10.1111/j.1755-2567.1970.tb00419.x.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact