Interprétation à la Curry-Howard pour les principes de choix – CHoICE

L’isomorphisme de Curry-Howard entre preuves mathématiques et programmes informatiques, initialement réservé aux langages purement fonctionnels, a depuis été étendu à de nouveaux paradigmes de programmation tels que les opérateurs de contrôle. De manière remarquable, l’ajout d’opérateurs de contrôle aux langages de programmation correspond, à travers l’isomorphisme de Curry-Howard, à l’ajout du tiers exclu aux systèmes logiques. Ce phénomène n’est pas isolé : l’ajout d’axiomes à un système logique correspond à l’ajout de primitives à un langage de programmation. Afin de pouvoir raisonner sur des langages de programmation de plus en plus expressifs il est nécessaire de trouver les axiomes que le système logique correspondant doit satisfaire. De manière duale, il s’avère fructueux de chercher, pour un axiome donné, son pendant calculatoire.

Ce projet propose d’appliquer cette méthodologie à différents principes de choix, omniprésents en mathématiques. L'axiome du choix usuel peut être exprimé sous de nombreuses variantes qui, bien qu'elles soient équivalentes dans un système logique muni du principe du tiers exclu, ne le sont plus dans un système intuitionniste. Par exemple, sous des hypothèses raisonnables, le tiers-exclus (incompatible avec certains cadres constructifs) peut se déduire de l'axiome du choix (exprimé en termes d'ensembles quotients). On peut donc affirmer que même les théories constructives ne parviennent pas à capturer pleinement la vraie nature de l’axiome du choix. À moyen terme, l'un des objectifs de ce projet consiste à se demander : quelle est l’interprétation calculatoire de l’axiome du choix ?
Cette question peut se décliner pour différente restriction de l'axiome du choix, e.g. le lemme de König, dont l'importance a été particulièrement souligné par les travaux en mathématiques à rebours. Ce projet peut-être vu comme une première étape en vue d'explorer un point de vue calculatoire pour les mathématiques à rebours constructives.