00:00:00 / 00:00:00

Appears in collection : Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométrique

Let A be a commutative ring. Does it have a maximal ideal? Classically, Zorn's lemma would allow us to concoct such an ideal. Constructively, no such ideal needs to exist. However, even though no maximal ideal might exist in the standard domain of discourse, a maximal ideal always exists ²somewhere². This is because every ring is countable ²somewhere², and ²everywhere², countable rings have maximal ideals. Concrete computational consequences follow from this phantomic variant of existence. The talk will introduce the modal operators 'somewhere' and 'everywhere', referring to the multiverse of parametrized mathematics, the multitude of computational forcing extensions. Just like the well-known double negation operator, they are (mostly) trivial from a classical point of view. Their purpose is to (a) put established results in constructive algebra and constructive combinatorics into perspective, (b) construct an origin story for certain inductive definitions and (c) form a unified framework for certain techniques for extracting programs from classical proofs. Our proposal is inspired by the study of the set-theoretic multiverse, but focuses less on exploring the range of set/topos-theoretic possibility and more on concrete applications in constructive mathematics. As guiding examples, we will examine algebraic closures of fields, Noetherian conditions on rings and the foundations of well-quasi orders such as Dickson's Lemma. (joint work with Alexander Oldenziel)

Information about the video

Citation data

  • DOI 10.24350/CIRM.V.20040003
  • Cite this video Blechschmidt Ingo (5/2/23). New modal operators for constructive mathematics. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.20040003
  • URL https://dx.doi.org/10.24350/CIRM.V.20040003



  • JOYAL, André et TIERNEY, Myles. An Extension of the Galois Theory of Grothendieck, volume 309 of Memoirs. American Mathematical Society, 1984.
  • BLASS, Andreas. Well-ordering and induction in intuitionistic logic and topoi. In : Mathematical logic and theoretical computer science. CRC Press, 2020. p. 29-48.
  • HENRY, Shawn J. Classifying Topoi and Preservation of Higher Order Logic by Geometric Morphisms. arXiv preprint arXiv:1305.3254, 2013. - https://doi.org/10.48550/arXiv.1305.3254

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow


  • Bookmark videos
  • Add videos to see later &
    keep your browsing history
  • Comment with the scientific
  • Get notification updates
    for your favorite subjects
Give feedback