Thursday 16 May 2019, 14:00, LSV library: Une structure logique unifiée pour l'axiome du choix, l'induction barrée et leurs principales conséquences, Hugo Herbelin (IRIF).

Les mathématiques à rebours de la théorie des ensembles établissent que l'axiome du choix a deux conséquences standard strictement plus faibles et mutuellement indépendantes : le théorème de l'ultrafiltre et l'axiome du choix dépendant, qui eux-mêmes, se rejoignent en losange (dans une théorie faible) pour prouver le lemme de König. De leur côté, les mathématiques à rebours intuitionnistes s'intéressent à l'induction barrée et au théorème de l'éventail dont on peut montrer qu'ils sont classiquement équivalents au choix dépendant et au lemme de König respectivement. (Accessoirement, un intérêt de l'induction barrée est de venir avec un contenu algorithme, la récursion barrée.) On donnera une classification précise des relations entre ces différents axiomes, montrant comment la contraposée d'une induction barrée généralisée fournit une version simple et unifiée de l'axiome du choix paramétrée par un domaine A et un codomaine B qui a la force du choix dépendant quand A est les entiers et la force du théorème de l'ultrafiltre quand B est les booléens. Cette approche soulignera aussi en quoi l'axiome du choix peut être vu comme un principe d'extensionalité relativement à la notion de "mauvaise" fondation.