Thèse Comparaison de la Force Logique des Théories des Ensembles et Théories des Types de Manière Constructive H/F - Doctorat.Gouv.Fr

Établissement : Université Paris-Saclay GS Informatique et sciences du numérique École doctorale : Sciences et Technologies de l'Information et de la Communication Laboratoire de recherche : Laboratoire Méthodes Formelles Direction de la thèse : Bruno BARRAS ORCID 0000000000000000 Début de la thèse : 2026-10-01 Date limite de candidature : 2026-05-12T23:59:59 L'objectif principal de cette thèse est de mieux définir la force logique du calcul des constructions inductives (CIC) en termes ensemblistes, et ce, dans un cadre intuitionniste. D'un point de vue pratique, nous prévoyons également d'implémenter des traductions entre les formalismes étudiés et de développer des outils pour rendre ces traductions utilisables en pratique.

La première partie consistera à établir un cadre permettant d'exprimer les preuves de cohérence relative dans toute leur généralité. Il s'agit notamment de distinguer clairement (1) les formalismes source et cible du résultat de cohérence relative et (2) la méta-théorie dans laquelle l'équivalence est réalisée. L'utilisation de Dedukti, un cadre logique, est envisagée.

La seconde partie consiste à démontrer des bornes plus précises pour la force du calcul des constructions inductives. Bien que l'on sache que les
types inductifs peuvent être interprétés dans une théorie des ensembles où l'on considère une forme plus faible d'axiome de remplacement (à savoir un axiome de récursion bien fondé),
il reste à comprendre comment interpréter les univers de la théorie des types dans ce cadre. Répondre à cette question pourrait nécessiter d'adapter le principe de réflexion à un cadre intuitionniste.
La comparaison entre théories des ensembles et théories des types a déjà été étudiée. Nous pouvons citer les travaux fondateurs d'Aczel. Plus spécifiquement pour CIC (la théorie de Rocq), Werner montre l'équivalence de ZFC avec l'extension de CIC par des axiomes de description et de choix. Toutefois, bien qu'il soit souvent fait la conjecture que CIC sans axiomes est bien plus faible que ZFC (et même probablement aussi ZF), il n'existe toujours pas de résultat précis à ce sujet. La question des univers est un point central dans cette étude.

D'autres travaux, notamment ceux de Rathjen, apportent des résultats de cohérence relative. Mais là encore, le cas de CIC sans axiomes n'est pas traité, et ces travaux se placent dans un cadre classique (i.e. supposant le tiers-exclu), ce qui pourrait être un obstacle pour disposer d'outils de traduction effectifs entre ces théories.
L'objectif de la thèse est de démontrer des résultats de cohérence
relative entre les théories des ensembles et les théories des
types. En particulier, on cherchera à affiner les résultats encadrant
la puissance du Calcul des Constructions Insductives (CIC, le
formalisme de Rocq) de la manière la plus fine.

Sur un aspect plus pratique, la réalisation d'outils permettant de
garantir la validité de ces preuves à un niveau formel, notamment en
garantissant que la preuve peut être encodée dans l'arithmétique du
premier ordre.

Un diplôme de mastère en informatique est requis, ainsi qu'une connaissance suffisante dans au moins un des domaines suivants:
- Foundations logiques, Théorie des modèles,
- Théories des Ensembles,
- Maitrise d'un système de preuve déductif (Rocq, Lean, Agda, etc.).