5 octobre 2020
Laura Fontanella (LACL)Attention salle inhabituelle : salle MSE 007.
La réalisabilité vise à extraire le contenu computationnel des preuves mathématiques en établissant une correspondance entre formules d’un système logique et programmes de telle manière que les `réalisateurs’ d’une formule démontrable dans le système (c. à d. les programmes qui sont associés à une telle formule via cette correspondance) nous fournissent des informations sur sa preuve.
Dans ce sens, la correspondance de Curry Howard peut être vu comme un résultat de réalisabilité. L’isomorphisme de Curry Howard établit une correspondance entre logique intuitionniste et lambda calcul simplement typé. Grâce aux travaux de Griffin et Krivine, la réalisabilité a ensuite évolué jusqu’à englober la logique classique d’abord, puis la théorie des ensembles. Les techniques développées par Krivine pour définir des modèles de réalisabilité pour la théorie des ensembles généralisent la méthode de Forcing, en fait les modèles de forcing sont des cas particulier de modèles de réalisabilité.
Nous allons aborder ces techniques et nous allons discuter les difficultés liées à la construction d’un modèle pour l’Axiome du Choix, je vous présenterai ainsi mes derniers résultats dans ce contexte fruit d’une collaboration avec Guillaume Geoffroy.