Évènement

Richard Matthews
University of Cambridge
https://richardmatthewslogic.github.io/

Date(s) : 20/06/2024   iCal
11h00 - 12h30

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 (ZFC).

Large cardinals are an important concept in set theory asserting the existence
of certain infinite sets satisfying additional properties, which in general
cannot be proven to exist from the axioms of ZFC. However, such sets are known
to provide significant structure to the set-theoretic universe, for example
giving the existence of Grothendieck universes and other universes satisfying
various closure properties. We shall show how to build Krivine style
realizability models for various large cardinal properties and present some
general results about ordinals and cardinals in these models. This is joint
work with Laura Fontanella and Guillaume Geoffroy.

Emplacement
I2M Luminy - TPR2, Salle de Séminaire 304-306 (3ème étage)

Catégories

• Séminaire