Séance de cours
Cette séance de cours traite de la structure logique des principes équivalents au choix et à l'induction de barre. Il commence par examiner le contrapositif de linduction de barre, conduisant à lintroduction dune notion généralisée de choix dépendant, appelée GDC, qui se rapporte à un prédicat sur les approximations finies des fonctions. L'instructeur décrit les forces de la GDC dans divers contextes, comme lorsque A est dénombrable ou lorsque B est un ensemble à deux éléments. La séance de cours couvre également les mathématiques inverses standard de l'axiome du choix, présentant des formulations équivalentes bien connues comme le lemme de Zorn et le principe de bon ordre. L'instructeur met l'accent sur les perspectives logiques et computationnelles de l'axiome du choix, soulignant comment les preuves intuitionnistes peuvent être considérées comme des programmes. Les contributions comprennent une classification des principes de choix et d'induction de barre et une discussion sur les principes de maximisation. La séance de cours se termine par un résumé des principaux résultats concernant le choix et l'induction de barre, illustrant les liens entre ces principes et leurs implications dans les mathématiques constructives.