Document Open Access Logo

From Co-Coverages to Radicals in Complete Lattices

Author Daniel Misselbeck-Wessel

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.74.pdf
  • Filesize: 0.93 MB
  • 29 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Proof theory
  • Theory of computation → Algebraic semantics
Keywords
  • Closure operator
  • prime element
  • spectrum
  • completeness theorem
  • point-free topology
  • transfinite method
  • dynamical algebra

Metrics

Abstract

Completeness and representation theorems in abstract algebra, lattice theory, and theoretical computer science are tied to the existence of ideal objects, and thus to transfinite methods such as Zorn’s lemma. Yet many concrete uses of those theorems appeal to finite approximations only, which carry a clear computational meaning. In this paper, we introduce co-coverages on complete lattices as a uniform way to specify ideal elements, and associate to each co-coverage a canonical closure operator with a folding property reminiscent of the covering principles at work in constructive algebra. This yields finitary, choice-free alternatives for arguments in which ideal objects are employed to reduce a computational problem to subcases. In a classical setting, our closure operators admit bases which allow to recover a host of primality principles such as the universal Krull–Lindenbaum theorem and Henkin’s lemma.

Cite As Get BibTex

Daniel Misselbeck-Wessel. From Co-Coverages to Radicals in Complete Lattices. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 74:1-74:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.74

Author Details

Daniel Misselbeck-Wessel
  • Munich Center for Mathematical Philosophy (MCMP), LMU Munich, Germany

Funding

Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - Project number 554603079.

Acknowledgements

This paper evolved from previous joint work with Peter Schuster, while ideas of Ingo Blechschmidt shaped its development in several ways. Vital momentum came from a lecture by Stefan Neuwirth on the philosophy of dynamical algebra, delivered at the 2022 autumn school "Proof and Computation", as well as from discussions with Dominik Kirst, made possible by a BayFrance mobility grant in 2025. The paper benefited greatly from three exceptionally careful and constructive reviews for LICS, for which the author is deeply grateful.

References

  1. Peter Aczel. An introduction to inductive definitions. In Jon Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 739-782. Elsevier Science B.V., Amsterdam, 1977. Google Scholar
  2. Peter Aczel and Michael Rathjen. Notes on constructive set theory. Technical report, Institut Mittag-Leffler, 2000. Report No. 40. Google Scholar
  3. Peter Aczel and Michael Rathjen. Constructive set theory. Book draft, 2010. URL: https://michrathjen.github.io/book.pdf.
  4. Shimshon A. Amitsur. A general theory of radicals. i. radicals in complete lattices. Amer. J. Math., 74(4):774-786, 1952. Google Scholar
  5. Shimshon A. Amitsur. A general theory of radicals. ii. radicals in rings and bicategories. Amer. J. Math., 76(1):100-125, 1954. Google Scholar
  6. Shimshon A. Amitsur. A general theory of radicals. iii. applications. Amer. J. Math., 76(1):126-136, 1954. Google Scholar
  7. Michael F. Atiyah and Ian G. Macdonald. Introduction to Commutative Algebra. Addison-Wesley, Reading, MA, 1969. Google Scholar
  8. Bernhard Banaschewski. A new proof that "Krull implies Zorn". Math. Log. Quart., 40:478-480, 1994. URL: https://doi.org/10.1002/MALQ.19940400405.
  9. Bernhard Banaschewski. Radical ideals and coherent frames. Comment. Math. Univ. Carolin., 37(2):349-370, 1996. Google Scholar
  10. Michael Beeson. Foundations of Constructive Mathematics. Springer-Verlag, Berlin, 1985. Google Scholar
  11. John L. Bell. Toposes and Local Set Theories: An Introduction. Number 14 in Oxford Logic Guides. Oxford University Press, Oxford, 1988. Google Scholar
  12. John L. Bell. Zorn’s lemma and complete Boolean algebras in intuitionistic type theories. J. Symb. Log., 62(4):1265-1279, 1997. URL: https://doi.org/10.2307/2275642.
  13. John L. Bell. Set Theory. Boolean-Valued Models and Independence Proofs. Oxford Logic Guides. Oxford University Press, Oxford, third edition, 2005. Google Scholar
  14. John L. Bell. The axiom of choice and the law of excluded middle in weak set theories. MLQ Math. Log. Q., 54:194-201, 2008. URL: https://doi.org/10.1002/MALQ.200710030.
  15. John L. Bell. Intuitionistic Set Theory. Number 50 in Studies in Logic. College Publications, 2014. Google Scholar
  16. Garrett Birkhoff. Lattice-ordered groups. Ann. Math., 43(2):298-331, 1942. Google Scholar
  17. Ingo Blechschmidt. Using the internal language of toposes in algebraic geometry. Doctoral dissertation, Universität Augsburg, 2017. Google Scholar
  18. Ingo Blechschmidt. Generalized spaces for constructive algebra. In Klaus Mainzer, Peter Schuster, and Helmut Schwichtenberg, editors, Proof and Computation II. From Proof Theory and Univalent Mathematics to Program Extraction and Verification, pages 99-187. World Scientific, Singapore, 2021. Google Scholar
  19. Ingo Blechschmidt and Peter Schuster. Maximal ideals in countable rings, constructively. In Ulrich Berger, Johanna N. Y. Franklin, Florin Manea, and Arno Pauly, editors, Revolutions and Revelations in Computability. 18th Conference on Computability in Europe, Lect. Notes Comput. Sci. Springer, 2022. Proceedings, CiE 2022, Swansea, Wales, July 11-15, 2022. URL: https://doi.org/10.1007/978-3-031-08740-0_3.
  20. Ingo Blechschmidt and Peter Schuster. Reifying dynamical algebra: maximal ideals in countable rings, constructively. Computability, 13:263-297, 2024. URL: https://doi.org/10.3233/COM-230454.
  21. Jan Cederquist and Thierry Coquand. Entailment relations and distributive lattices. In Samuel R. Buss, Petr Hájek, and Pavel Pudlák, editors, Logic Colloquium '98. Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Prague, Czech Republic, August 9-15, 1998, volume 13 of Lect. Notes Logic, pages 127-139. A. K. Peters, Natick, MA, 2000. Google Scholar
  22. C.C. Chang. A new proof of the completeness of the Lukasiewicz axioms. Trans. Am. Math. Soc., 93(1):74-80, 1959. Google Scholar
  23. Francesco Ciraulo, Maria Emilia Maietti, and Giovanni Sambin. Convergence in formal topology: a unifying notion. J. Log. Anal., 5(2):1-45, 2013. URL: http://logicandanalysis.org/index.php/jla/article/view/196/82.
  24. Thierry Coquand. Constructive algebra and point-free topology. In Douglas Bridges, Hajime Ishihara, Michael Rathjen, and Helmut Schwichtenberg, editors, Handbook of Constructive Mathematics, pages 150-167. Cambridge University Press, 2023. Google Scholar
  25. Thierry Coquand and Henri Lombardi. Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative rings. In M. Fontana, S.-E. Kabbaj, and S. Wiegand, editors, Commutative Ring Theory and Applications, volume 231 of Lect. Notes Pure Appl. Mathematics, pages 477-499, Reading, MA, 2002. Addison-Wesley. Google Scholar
  26. Thierry Coquand and Henri Lombardi. A logical approach to abstract algebra. Math. Structures Comput. Sci., 16:885-900, 2006. URL: https://doi.org/10.1017/S0960129506005627.
  27. Thierry Coquand, Henri Lombardi, and Stefan Neuwirth. Lattice-ordered groups generated by an ordered group and regular systems of ideals. Rocky Mountain J. Math., 49(5):1449-1489, 2019. Google Scholar
  28. Thierry Coquand, Henri Lombardi, and Stefan Neuwirth. An introduction to Lorenzen’s `Algebraic and Logistic Investigations on Free Lattices' (1951). Hist. Philos. Logic, 46(4):525-545, 2025. Google Scholar
  29. Thierry Coquand, Henri Lombardi, and Claude Quitté. Dimension de Heitmann des treillis distributifs et des anneaux commutatifs. Publications Mathématiques de Besançon. Algèbre et Théorie des Nombres, pages 57-100, 2006. Google Scholar
  30. Michel Coste, Henri Lombardi, and Marie-Françoise Roy. Dynamical method in algebra: Effective Nullstellensätze. Ann. Pure Appl. Logic, 111(3):203-256, 2001. URL: https://doi.org/10.1016/S0168-0072(01)00026-4.
  31. Laura Crosilla. Exploring predicativity. In Klaus Mainzer, Peter Schuster, and Helmut Schwichtenberg, editors, Proof and Computation, pages 83-108. World Scientific, Singapore, 2018. Google Scholar
  32. Laura Crosilla. Set Theory: Constructive and Intuitionistic ZF. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Winter 2024 edition, 2024. Google Scholar
  33. Giovanni Curi. On Tarski’s fixed point theorem. Proc. Amer. Math. Soc., 143(10):4439-4455, 2015. Google Scholar
  34. Radu Diaconescu. Axiom of choice and complementation. Proc. Amer. Math. Soc., 51(1):176-178, 1975. Google Scholar
  35. M. Erné, J. Koslowski, A. Melton, and G.E. Strecker. A primer on Galois connections. Ann. N. Y. Acad. Sci., 704(1):103-125, 1993. Google Scholar
  36. Marcel Erné. Distributors and wallmanufacture. J. Pure Appl. Algebra, 68:109-125, 1990. Google Scholar
  37. Marcel Erné. Distributors and Wallman locales. Houston J. Math., 34(1):69-98, 2008. Google Scholar
  38. Giulio Fellin. The Jacobson Radical: from Algebra to Logic, 2018. Master’s thesis. Università di Verona, Dipartimento di Informatica. Google Scholar
  39. Giulio Fellin. A unifying conservation theorem. In Stefano Guerrini and Barbara König, editors, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026), volume 363 of Leibniz International Proceedings in Informatics, pages 4:1-44:23, Paris, 2026. URL: https://doi.org/10.4230/LIPIcs.CSL.2026.19.
  40. Giulio Fellin, Sara Negri, and Peter Schuster. Nuclear shifts for conservation. In Vasco Brattka, Henning Fernau, and Lorenzo Galeotti, editors, Timeless Machines: Computability Across Eras. 21st Conference on Computability in Europe. forthcoming, 2026. Proceedings, CiE 2026, Trier, Germany, July 27-31, 2026. Google Scholar
  41. Giulio Fellin and Peter Schuster. A general Glivenko-Gödel theorem for nuclei. In Ana Sokolova, 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. Elsevier, 2021. Google Scholar
  42. Giulio Fellin and Peter Schuster. Conservation as translation. Rev. Symb. Log., 18(1):316-348, 2025. URL: https://doi.org/10.1017/S1755020324000170.
  43. Giulio Fellin, Peter Schuster, and Daniel Wessel. The Jacobson radical of a propositional theory. Bull. Symbolic Logic, 28(2):163-181, 2022. URL: https://doi.org/10.1017/BSL.2021.66.
  44. Ralph Freese, Ježek, and J.B. Nation. Free Lattices, volume 42 of Mathematical Surveys and Monographs. American Mathematical Society, Providence, Rhode Island, 1995. Google Scholar
  45. Harvey Friedman. The consistency of classical set theory relative to a set theory with intuitionistic logic. The Journal of Symbolic Logic, 38(2):315-319, 1973. URL: https://doi.org/10.2307/2272068.
  46. B. J. Gardner and R. Wiegandt. Radical Theory of Rings. Marcel Dekker, Inc., New York, 2004. Google Scholar
  47. Mai Gehrke and Sam van Gool. Topological Duality for Distributive Lattices. Theory and Applications. Cambridge University Press, 2024. Google Scholar
  48. G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, Berlin, 1980. Google Scholar
  49. Nicolas D. Goodman and John Myhill. Choice implies excluded middle. Z. Math. Logik Grundlagen Math., 24:461, 1978. URL: https://doi.org/10.1002/MALQ.19780242514.
  50. Timothy Gowers. VI. The ABC Conjecture. In Timothy Gowers, editor, The Princeton Companion to Mathematics. Princeton University Press, Princeton, 2008. June Barrow-Green and Imre Leader (associate editors). Google Scholar
  51. George Grätzer. Lattice Theory: Foundation. Birkhäuser, Basel, 2011. Google Scholar
  52. Leon Henkin. The completeness of the first-order functional calculus. J. Symb. Log., 14:159-166, 1949. URL: https://doi.org/10.2307/2267044.
  53. Wilfried Hodges. Krull implies Zorn. J. Lond. Math. Soc., 19:285-287, 1979. Google Scholar
  54. Paul Howard and Jean Rubin. Consequences of the Axiom of Choice. American Mathematical Society, Providence, RI, 1998. Google Scholar
  55. Hajime Ishihara. Classical propositional logic and decidability of variables in intuitionistic propositional logic. Log. Methods Comput. Sci., 10(3):3:1, 7, 2014. URL: https://doi.org/10.2168/LMCS-10(3:1)2014.
  56. Ute Isphording. Theorie des Radikals auf verbandstheoretischer Grundlage. Doctoral dissertation, Universität München, 1966. Google Scholar
  57. Peter T. Johnstone. Stone Spaces, volume 3 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982. Google Scholar
  58. Peter T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium. Vol. 2, volume 44 of Oxford Logic Guides. The Clarendon Press Oxford University Press, Oxford, 2002. Google Scholar
  59. Tatsuji Kawai. Geometric theories of patch and Lawson topologies. Preprint, 2017. URL: https://arxiv.org/abs/1709.06403.
  60. Edward Kissin, Victor Shulman, and Yuri Turovskii. Relations and radicals in abstract lattices and in lattices of subspaces of banach spaces and of ideals of banach algebras. amitsur’s theory revisited. Order, 38:143-201, 2021. URL: https://doi.org/10.1007/S11083-020-09533-4.
  61. Wolfgang Krull. Idealtheorie in Ringen ohne Endlichkeitsbedingung. Math. Ann., 101:729-744, 1929. Google Scholar
  62. Henri Lombardi. Spectral spaces versus distributive lattices: A dictionary. In A. Facchini, M. Fontana, A. Geroldinger, and B. Olberding, editors, Advances in Rings, Modules and Factorizations 2018, volume 213 of Springer Proceedings in Mathematics & Statistics. Springer, Cham, 2020. Google Scholar
  63. Henri Lombardi and Claude Quitté. Commutative Algebra: Constructive Methods. Finite Projective Modules, volume 20 of Algebra and Applications. Springer Netherlands, Dordrecht, 2015. Google Scholar
  64. Paul Lorenzen. Algebraische und logistische Untersuchungen über freie Verbände. J. Symb. Logic, 16(2):81-106, 1951. URL: https://doi.org/10.2307/2266681.
  65. Ray Mines, Fred Richman, and Wim Ruitenburg. A Course in Constructive Algebra. Springer, New York, 1988. Universitext. Google Scholar
  66. Daniel Misselbeck-Wessel. Good sequences without subdirect representation: a constructive treatment of Mundici’s Γ functor. Stud. Logica, 2026. URL: https://doi.org/10.1007/s11225-026-10236-x.
  67. Daniel Misselbeck-Wessel and Peter Schuster. Radical theory of Scott-open filters. Theoret. Comput. Sci, 945, 2023. Paper 113677. URL: https://doi.org/10.1016/J.TCS.2022.12.027.
  68. Sara Negri and Jan von Plato. Structural Proof Theory. Cambridge University Press, Cambridge, 2001. Google Scholar
  69. Stefan Neuwirth. Lorenzen’s reshaping of Krull’s Fundamentalsatz for integral domains (1938-1953). In Gerhard Heinzmann and Gereon Wolters, editors, Paul Lorenzen: Mathematician and Logician, volume 51 of Logic, Epistemology, and the Unity of Science, pages 143-183. Springer, Cham, 2021. Google Scholar
  70. Oystein Ore. Theory of equivalence relations. Duke Math. J., 9(3):573-627, 1942. Google Scholar
  71. Jorge Picado and Aleš Pultr. Frames and Locales. Topology without Points. Frontiers in Mathematics. Birkhäuser, Basel, 2012. Google Scholar
  72. Carl J. Posy. Mathematical Intuitionism. Elements in the Philosophy of Mathematics. Cambridge University Press, Cambridge, 2020. Google Scholar
  73. George N. Raney. Completely distributive complete lattices. Proc. Am. Math. Soc., 3(5):677-680, 1952. Google Scholar
  74. Michael Rathjen. An introduction to constructive set theory: An appetizer. In Douglas Bridges, Hajime Ishihara, Michael Rathjen, and Helmut Schwichtenberg, editors, Handbook of Constructive Mathematics, pages 20-60. Cambridge University Press, 2023. Google Scholar
  75. Davide Rinaldi and Peter Schuster. A universal Krull-Lindenbaum theorem. J. Pure Appl. Algebra, 220:3207-3232, 2016. Google Scholar
  76. Davide Rinaldi, Peter Schuster, and Daniel Wessel. Eliminating disjunctions by disjunction elimination. Indag. Math. (N.S.), 29(1):226-259, 2018. Communicated first in Bull. Symb. Logic 23 (2017), 181-200. Google Scholar
  77. Davide Rinaldi and Daniel Wessel. Cut elimination for entailment relations. Arch. Math. Logic, 58(5-6):605-625, 2019. URL: https://doi.org/10.1007/S00153-018-0653-0.
  78. Kimmo I. Rosenthal. Quantales and their Applications, volume 234 of Pitman Research Notes in Mathematics. Longman Scientific & Technical, Essex, 1990. Google Scholar
  79. Giovanni Sambin. Intuitionistic formal spaces - a first communication. In D. Skordev, editor, Mathematical Logic and its Applications, Proc. Adv. Internat. Summer School Conf., Druzhba, Bulgaria, 1986, pages 187-204. Plenum, New York, 1987. Google Scholar
  80. Giovanni Sambin. Some points in formal topology. Theoret. Comput. Sci., 305(1-3):347-408, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00704-1.
  81. Giovanni Sambin. Positive Topology: A New Practice in Constructive Mathematics. Oxford University Press, 2025. Google Scholar
  82. Andrej Scedrov. Intuitionistic set theory. In L.A. Harrington, M.D. Morley, A. Scedrov, and S.G. Simpson, editors, Harvey Friedman’s Research on the Foundations of Mathematics, volume 117 of Studies in Logic and the Foundations of Mathematics, pages 257-284. Elsevier, 1985. Google Scholar
  83. Peter Schuster. Induction in algebra: a first case study. In 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, pages 581-585. IEEE Computer Society Publications, 2012. Logical Methods in Computer Science (3:20) 9 (2013). URL: https://doi.org/10.1109/LICS.2012.68.
  84. Peter Schuster and Daniel Wessel. 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, pages 820-830, New York, NY, USA, 2020. Association for Computing Machinery. Google Scholar
  85. Peter Schuster and Daniel Wessel. The Jacobson radical for an inconsistency predicate. Computability, 11(2):147-162, 2022. URL: https://doi.org/10.3233/COM-210365.
  86. Peter Schuster, Daniel Wessel, and Ihsen Yengui. Dynamic evaluation of integrity and the computational content of Krull’s lemma. J. Pure Appl. Algebra, 226(1), 2022. Paper 106794. Google Scholar
  87. Peter Schuster and Ihsen Yengui. An iterative constructive Hilbert basis theorem. J. Algebra, 676:56-68, 2025. Google Scholar
  88. Dana Scott. Completeness and axiomatizability in many-valued logic. In Leon Henkin, John Addison, C.C. Chang, William Craig, Dana Scott, and Robert Vaught, editors, Proceedings of the Tarski Symposium (Proc. Sympos. Pure Math., Vol. XXV, Univ. California, Berkeley, Calif., 1971), pages 411-435. Amer. Math. Soc., Providence, RI, 1974. Google Scholar
  89. Ian Shillito and Dominik Kirst. A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, pages 218-229, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3636501.3636957.
  90. D. J. Shoesmith and T. J. Smiley. Multiple-Conclusion Logic. Cambridge University Press, Cambridge, 1978. Google Scholar
  91. Josef Šlapal. On bases of closure operators on complete lattices. Quaestiones Math., 46(4):781-790, 2023. Google Scholar
  92. Morten Heine Sørensen and Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, Amsterdam, 2006. Google Scholar
  93. Bo Stenström. Radicals and socles of lattices. Arch. Math., 20:258-261, 1969. Google Scholar
  94. Benno van den Berg. Non-deterministic inductive definitions. Arch. Math. Logic, 52(1-2):113-135, 2013. URL: https://doi.org/10.1007/S00153-012-0309-4.
  95. Benno van den Berg. A Kuroda-style j-translation. Arch. Math. Log., 58:627-634, 2019. URL: https://doi.org/10.1007/s00153-018-0656-x.
  96. Steven Vickers. Topology via logic, volume 5 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989. Google Scholar
  97. Daniel Wessel. A note on connected reduced rings. J. Comm. Algebra, 13(4):583-588, 2021. Google Scholar
  98. Glynn Winskel. On powerdomains and modality. Theoret. Comput. Sci., 36:127-137, 1985. URL: https://doi.org/10.1016/0304-3975(85)90037-4.
  99. Ihsen Yengui. Making the use of maximal ideals constructive. Theoret. Comput. Sci., 392:174-178, 2008. URL: https://doi.org/10.1016/J.TCS.2007.10.011.
  100. Ihsen Yengui. Constructive Commutative Algebra. Projective Modules over Polynomial Rings and Dynamical Gröbner Bases, volume 2138 of Lecture Notes in Mathematics. Springer, Cham, 2015. Google Scholar
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact