Une interprétation générale du Fan Theorem par réalisabilité
Titouan Leclercq
I2M, Aix-Marseille
Date(s) : 26/03/2026 iCal
11h00 - 12h30
Le Fan Theorem (FT) de Brouwer est un résultat central en mathématiques
constructives, qui établit une notion de continuité. Ce résultat n’est
cependant par vrai en général : en particulier, certains modèles de
réalisabilité ne le satisfont pas. Il existe pour autant d’autres modèles qui
vérifient FT, comme la seconde algèbre de réalisabilité (K2) de Kleene.
En 2013, Lubarsky et Rathjen ont donné un autre modèle de réalisabilité qui
satisfait FT, qui a la particularité d’utiliser comme réaliseurs des fonctions
plus faibles que pour K2. Sur la base de ce travail, nous construisons un
nouveau modèle réalisant FT et basé sur un lambda-calcul avec oracles.
Grâce à ce modèle et en utilisant la notion d’Evidenced Frame, nous donnons un
théorème général donnant des conditions suffisantes pour n’importe quel système
de calcul pour que son interprétation de réalisabilité satisfasse FT. Nous
pensons que cette méthode peut permettre de mieux comprendre le contenu
calculatoire d’autres axiomes, en construisant des théorèmes portant sur des
notions suffisamment générales de systèmes de calcul.
Dans cette présentation, je vais décrire le modèle de réalisabilité inspiré par
le travail de Lubarky et Rathjen (après avoir rappelé l’énoncé de FT ainsi que
le fonctionnement de la réalisabilité), puis présenter comment généraliser
l’argument à un cas général de système de calcul.
Ce travail a été réalisé en collaboration avec Etienne Miquey.
Emplacement
I2M Luminy - TPR2, Salle de Séminaire 304-306 (3ème étage)
Catégories
