11 décembre 2023
Richard Matthews (LACL)The method of realizability was first developed by Kleene and is seen as a way to extract computational content from mathematical proofs via the Curry-Howard Correspondence. The Curry-Howard Correspondence is a way to associate with each mathematical proof a computer program. Then, from a theorem one can extract computational content by analysing the programs associated to the proof of the statement. Traditionally, this method was restricted to producing models which satisfied intuitionistic logic; however it was later extended by Krivine to produce models which satisfy full classical logic and even Zermelo-Fraenkel set theory with choice. In this talk we will discuss Krivine’s method to construct realizability models of ZF and what this reveals about the computational content of set theory with respect to the Curry-Howard Correspondence. We will then present recent results concerning ordinals and cardinals in these realizability models. This is joint work with Laura Fontanella and Guillaume Geoffroy.