La jerarquía analítica ramificada en lógica de segundo orden

Cette thèse s'intéresse dans un premier temps à l'étude de la hiérarchie analytique ramifiée (RAH) en arithmétique du second ordre (PA2). La hiérarchie analytique ramifiée a été définie par Kleene en 1960. C'est une adaptation de la notion de constructibilité (introduite par Gödel pour la théorie des ensembles) au cadre de l'arithmétique du second ordre. Les propriétés de cette hiérarchie, en relation avec la théorie de la récursion et l'étude des modèles ensemblistes de PA2, ont été étudiées en profondeur. Il semble naturel de formaliser RAH dans PA2 pour essayer de démontrer qu'ajouter l'axiome du choix ou (une variante de) l'axiome de constructibilité à PA2 n'apporte pas de contradiction. Cependant, la seule trace écrite d'une telle formalisation semble incorrecte. Dans cette thèse, nous souhaitons travailler sur cette formalisation. Pour cela, nous allons travailler dans une version de l'arithmétique obtenue en enlevant l'axiome d'induction des axiomes de PA2. Dans ce système, une nouvelle variante de l'axiome du choix apparaît : nous l'appelons l'axiome de collection, en référence à l'axiome de théorie des ensembles portant le même nom. Cet axiome semble n'avoir jamais été considéré dans le cadre de la logique du second ordre. Nous montrons qu'il a de bonnes propriétés calculatoires : sa contraposée est réalisée par l'identité en réalisabilité classique alors qu'il est lui-même réalisé par l'identité en réalisabilité intuitionniste. De plus, nous en énonçons une forme équivalente qui est interprétée par une traduction négative de la logique classique vers la logique intuitionniste. Enfin, nous montrons qu'une variante de cet axiome est plus faible qu'une variante de l'axiome du choix en logique intuitionniste. Nous travaillons donc dans une théorie sans induction mais contenant l'axiome de collection pour étudier la hiérarchie analytique ramifiée. Nous montrons que c'est un modèle de PA2 satisfaisant une version forte d'axiome du choix : le principe de l'univers bien ordonné. Il nous semble que l'axiome de collection est nécessaire et nous donnons des arguments pour expliquer cette intuition. Dans une deuxième partie de la thèse, plus courte que la première, nous étudions l'égalité extensionnelle en arithmétique des types finis (HAw). L'arithmétique des types finis est une extension conservative de l'arithmétique de Heyting obtenue en étendant la syntaxe des termes à tout le Système T. Elle parle donc des fonctionnelles de types finis. Alors que l'égalité entre entiers naturels est spécifiée par les axiomes de Peano, comment peut être définie l'égalité entre fonctionnelles ? Différentes réponses à cette question poussent à l'étude de différentes variantes de HAw, telles qu'une variante extensionnelle (E-HAw) où deux fonctionnelles sont égales si elles ont le même graphe. Dans cette partie, nous allons montrer comment l'étude d'une famille de relations d'équivalence partielle nous amène à définir une interprétation par paramétricité de l'égalité extensionnelle dans HAw.