Séminaires : Séminaire de Logique Lyon-Paris

Equipe(s) : lm,
Responsables :O. Finkel, A. Khélif, S. Rideau, T. Tsankov, A. Vignati
Email des responsables :
Salle : Zoom ID: 824 8220 9628; s'inscrire à la liste ou contacter silvain.rideau@imj-prg.fr pour le mot de passe.
Adresse :
Description

ArchivesRetour ligne automatique
Abonnement à la liste de diffusion


Orateur(s) Hadrien Batmalle - IRIF, Université Paris Diderot,
Titre Forcing, réalisabilité classique et propriétés de préservation
Date26/11/2018
Horaire15:10 à 16:10
Diffusion
RésumeLa réalisabilité classique est une technique d'interprétation des énoncés d'une théorie par des programmes. Elle permet de construire des modèles et apparaît comme une généralisation du forcing. Si l'interprétation de théorèmes par des programmes a un intérêt évident en informatique, l'étude des modèles de ZF obtenus par réalisabilité classique est aussi intéressante en soi: en effet, sauf dans les cas dégénérés, ces modèles sont très différents des modèles de forcing; par exemple ils ne conservent pas les ordinaux. Cela permet d'exhiber des propriétés pathologiques qu'on ne savait pas obtenir précédemment (on a donc un outil supplémentaire pour les preuves d'indépendance) mais présente aussi de nouvelles difficultés. En particulier, si on sait bien souvent en forcing quels sont les critères que doit vérifier la structure des conditions pour obtenir telle ou telle propriété dans le nouveau modèle, la réalisabilité est, pour le moment, beaucoup plus difficile à aborder. On présentera ici quelques
techniques récentes de réalisabilité classique à rapprocher de techniques bien connues en forcing: l'opérateur de bar-récursion, qui joue un rôle analogue aux ensembles de conditions omega-clos (Krivine 2014) et un nouveau résultat de transfert de propriétés du modèle de départ qui est utilisé dans les mêmes situations que des critères de type conditions d'antichaîne. On appliquera ce dernier résultat à la construction de modèles de réalisabilité pour la négation du choix dénombrable et la négation de l'hypothèse du continu, et donc de programmes réalisant ces énoncés.
SalleZoom ID: 824 8220 9628; s'inscrire à la liste ou contacter silvain.rideau@imj-prg.fr pour le mot de passe.
Adresse
© IMJ-PRG