The computational content of set theory – COCONTENS

This is an interdisciplinary project combining tools from set theory and theoretical computer science. The main purpose of this project is to study the computational content of set theory through realizability models. Realizability is a branch of logic that aims at extracting the computational content of mathematical theories by establishing proof-as-programs correspondences (this process is at the heart of the programs extraction in proofs assistants such as Coq). Developed by Kleene within research in constructive mathematics, modern realizability extends the Curry Howard Isomorphism and has evolved to include first classical logic, then even set theory thanks to the work of J-L. Krivine. Krivine’s technique generalizes the method of Forcing and enable us to extract the computational content of the theory of sets ZF. While this method works well for ZF, the Axiom of Choice, AC is more problematic. In 2003, Krivine proved that a non extensional version of AC could be realized using the `quote' instruction of LISP and that was enough to realize Dependent Choice, DC. DC corresponds to a countable version of AC, but in 2020 Fontanella and Geoffroy proved that it is possible to realize even uncountable versions of AC, by considering programs that generalize 'quote'. Recently Krivine found a realizability model for the full AC, however, it is not clear from this model which programs realize AC. In continuation with these results, this project will focus on 3 main objectives:
1. Extract the computational content of AC by individuating a program that realizes it
2. Extract the computational content of other axioms or principles that can be proven consistent with ZF by Forcing (ex. CH, not CH, MA...)
3. Extract the computational content of other axioms that can be proven consistent with inner models (ex. V=L)