00:00:00 / 00:00:00

Apparaît dans la 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)

Informations sur la vidéo

Données de citation

  • DOI 10.24350/CIRM.V.20040003
  • Citer cette vidéo Blechschmidt Ingo (02/05/2023). 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

Dernières questions liées sur MathOverflow

Pour poser une question, votre compte Carmin.tv doit être connecté à mathoverflow

Poser une question sur MathOverflow


  • Mettez des vidéos en favori
  • Ajoutez des vidéos à regarder plus tard &
    conservez votre historique de consultation
  • Commentez avec la communauté
  • Recevez des notifications de mise à jour
    de vos sujets favoris
Donner son avis