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)