Le topos des types et le topos des filtres en logique categorique

Nous abordons dans la presente these deux constructions analogues de logique categorique. Nous etudions tout d'abord ces constructions dans le contexte de doctrines propositionnelles.;La premiere que nous etudions portes dans le contexte propositionnel, le nom de: "double dual". Nous la retrouvons principalement exposee dans l'article de Makkai et Reyes [25]. La deuxieme construction qui nous interesse est celle du locale des filtres; etudiee par Pitts dans [29]. Ces deux constructions ont, deja au niveau propositionnel, des proprietes remarquables. Nous explorons, dans les deux premiers chapitres, le portrait global a propos de ces deux constructions propositionnelles. Nous les regardons individuellement en etalant leurs proprietes de base; dont leur(s) propriete(s) universelle(s) ou quasi-universelle. Puis, nous les comparons et donnons des conditions pour quelles co&;La deuxieme facette de cette these, quant a elle, est une exploration d'un niveau de complexite superieur. Nous y retrouvons encore une fois les deux memes constructions mais, cette fois-ci, dans le contexte de la logique du premier ordre. Nous generalisons les resultats importants des premiers chapitres a ce nouveau contexte. Dans le chapitre 3 nous etudions la categorie des filtres et construisons avec cette notion le topos des filtres (en suivant [31]). Nous demontrons une propriete quasi-universelle du topos des filtres parmis les f-modeles (notion analogue a la notion de p-modele) dans un topos completement distributif. Dans le chapitre 4 nous etudions le topos des types. Nous demontrons une propriete universelle pour cette construction plus generale que celle originalement donnee dans Makkai dans [23]. Dans le chapitre 5 nous comparons le topos des types et le topos des filtres et generalisons ainsi des resultats du chapitre 2. Puis, nous comparons le topos des filtres au topos classifiant et donnons des conditions pour que ces deux coincident. Finalement, nous demontrons que les fondeurs sous-jacents au topos des types et au topos des filtres reflechissent les isomorphismes commme dans le cas propositionnel. Nous utilisons principalement les outils de la theorie des topos et de la theorie des faisceaux pour accomplir notre exploration.