Une étude fibrationelle des topos de réalisabilité
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
This thesis is a contribution to categorical logic, in particular to the theory of realizability toposes. While the tools of categorical logic have proven very successful in analyzing and organizing proof theoretic realizabilit) interpretations, it was retnarked by experts (notably Peter Johnstone) that the field of realizability toposes itself was not clearly delineated, and lacked a powerful theory theory analogous to that of Grothendieck toposes. The présent work sets out to remedy this situation to a certain extent. We argue that realizability toposes are best understood using Grothendieck fibrations, and develop a framework of fibrational cocompletions, which allows to view certain constructions from realizability in precise analogy to constructions of presheaf and sheaf toposes. Using these techniques, and a clans of posetal fibrations that we cati uniform preorders, we are able to give an extensional characterization of partial combinatory algebras and of the realizability toposes that are constructed from these algebras. Striving to develop the analogy to Grothendieck toposes further, we outline how to apply our techniques on arbitrary ba: toposes, and give a decomposition theorem for constant objects functors induced by triposes, analogous to the known decompositions of geometric tnorphisms. Finally, we sketch an approach of how to find a unified frainework for Grothendieck toposes and realizability toposes, based on the observation that uniform preorders can be identified with preorders internai to a category of sheaves.
Abstract FR:
Cette thèse est une contribution à la logique catégorique, plus précisement à la théorie des topos de réalisabilité. Bien que les outils de la logique catégorique aient été très fructueux dans l'analyse et l'organisation des interprétations de réalisabilité provenant de la théorie de la démonstration, des experts (notamment Peter Johnstone) ont remarqué que le domaine des topos de réalisabilité n'a pas été clairement délimité, et qu'il manquait une théorie puissante semblable à celle des topos de Grothendieck. Le but de cette thèse est de remédier à cela dans une certaine mesure. Nous affirmons que le contexte naturel pour analyser les topos de réalisabilité est les fibrations de Grothendieck, et nous élaborons un cadre de cocomplétions fibrationnelles, permettant de voir certaines constructions de réalisabilité comme des constructions de préfaisceaux et faisceaux. Grâce à cela, et en utilisant une classe de fibrations posetales que nous appelons des préordres uniformes, nou donnons une caractérisation extensionelle des algèbres combinatoires partielles et des topos de réalisabilité construits à partir de ces algèbres. Poursuivant l'analogie avec les topos de Grothendieck, nous décrivons comment appliquer nos techniques à des topos de base arbitraires, et donnons un théorème de décomposition des fonçteurs d'objets constants provenant des triposes, semblable aux décompositions des morphismes géométriques. Enfin, nous esquissons les contours d'un cadre unifié entre les topos de Grothendieck et les topos de réalisabilité, utilisant comme point de départ l'identification des préordres uniformes avec les préordres internes à une catégorie de faisceaux.