Laura Fontanella (Université Paris-Est Créteil)
- Date
- Wednesday 11 November 2020
- Category
- Models and Sets Seminar
Realizability and the Axiom of Choice
Realizability aims at extracting the computational content of mathematical proofs. Introduced in 1945 by Kleene as part of a broader program in constructive mathematics, realizability has later evolved to include classical logic and even set theory. Recent methods that generalize the technique of Forcing led to define realizability models for the theory ZF, but realizing the Axiom of Choice remains problematic. After a brief presentation of these methods, we will discuss the major obstacles for realizing the Axiom of Choice and I will present my recent joint work with Guillaume Geoffroy that led to realize weak versions of the Axiom of Choice.