Réalisabilité classique : nouveaux outils et applications

Résumé fourni par la source

La realisabilite classique de Jean-Louis Krivine associe a chaque modele de calcul et chaque modele de la theorie des ensembles un nouveau modele de la theorie des ensembles, appele modele de realisabilite, d'une facon similaire au forcing. Chaque modele de realisabilite est muni d’une algebre de Boole caracteristique $\gimel 2$ (gimel 2), dont la structure donne des informations sur les proprietes du modele de realisabilite. En particulier, les modeles de forcing correspondent au cas ou $\gimel 2$ est l'algebre de Boole a deux elements. Ce travail presente de nouveaux outils pour manipuler les modeles de realisabilite et donne de nouveaux resultats obtenus en les exploitant. L'un d'entre eux est qu'au premier ordre, la theorie des algebres de Boole a au moins deux elements est complete pour $\gimel 2$, au sens ou $\gimel 2$ eut etre rendue elementairement equivalente a n'importe quelle algebre de Boole. Deux autres resultats montrent que $\gimel 2$ peut etre utilisee pour etudier les modeles denotationnels de langage de programmation (chacun part d'un modele denotationnel et classifie ses degres de parallelisme a l'aide de $\gimel 2$). Un autre resultat montre que la technique de Jean-Louis Krivine pour realiser l'axiome des choix dependants a partir de l'instruction quote peut se generaliser a des formes plus fortes de choix. Enfin, un dernier resultat, obtenu en collaboration avec Laura Fontanella, accompagne le precedent en adaptant la condition d'antichaine denombrable du forcing au cadre de la realisabilite, ce qui semble semble ouvrir une piste prometteuse pour realiser l'axiome du choix.