|
|
|
PETITE ÉCOLE SUR
LES FAISCEAUX
EN LOGIQUE ET EN GÉOMÉTRIE
Avec des interventions de:
Boas EREZ, François LAMARCHE, Paul-André MELLIÈS
« Le thème du topos est issu de celui des schémas, l’année même où sont apparus les schémas - mais en étendue il dépasse largement le thème-mère. C’est le thème du topos, et non celui des schémas, qui est ce "lit", ou cette "rivière profonde", où viennent s’épouser la géométrie et l’algèbre, la topologie et l’arithmétique, la logique mathématique et la théorie des catégories, le monde du continu et celui des structures "discontinues" ou "discrètes". Si le thème des schémas est comme le coeur de la géométrie nouvelle, le thème du topos en est l’enveloppe, ou la demeure. Il est ce que j’ai conçu de plus vaste, pour saisir avec finesse, par un même langage riche en résonances géométriques, une "essence" commune à des situations des plus éloignées les unes des autres, provenant de telle région ou de telle autre du vaste univers des choses mathématiques. »
Alexandre GROTHENDIECK, Récoltes et semailles, p. 43
Lieu et horaires:
- bâtiment A33 (présidence/maths) étage 2 salle 2 (plan du campus Bx1)
- les vendredis de 16:00 à 17:00
Objectifs
Cette petite école est destinée aux collègues et aux doctorants en informatique ou en mathématiques (ces derniers pourront comptabiliser ces heures dans le cadre de leur formation doctorale). Elle demandera un peu d'indulgence aux participants car les intervenants ne maîtrisent pas d'avance l'ensemble des sujets qu'ils vont pourtant tenter de présenter.
Il s'agit avant tout de découvrir les modèles mathématiquement naturels de la logique intuitionniste construits sur les notions de faisceau et de topos. Initiée par Grothendieck dans le cadre de la géométrie algébrique, l'étude logique des topoi a été principalement poursuivie, dans le sillage de Lawvere, par des catégoriciens.
Cette école devrait déboucher sur quelques questions ouvertes, comme la définition de modèles complets pour la logique linéaire du premier ordre (avec des applications prometteuses au typage sémantique en linguistique formelle comme à la spécification de programmes).
Documents:
Séances:
- 9 octobre (J. G. & Ch. R.)
- Présentation de l'école, motivations
- Un peu de logique: langages, preuves, modèles
- calcul propositionnel: langage, valuation, séquents, complétude et compacité
- 16 octobre (Ch. R.)
- Un peu de logique (suite): langages, preuves, modèles
- calcul des prédicats: langage, valuation, séquents, complétude et compacité
- 23 octobre (Ch. R.)
- Un peu de logique (fin): langages, preuves, modèles
- calcul des prédicats: démonstration du théorème de complétude
(Gödel 1930 méthode de Henkin 1949)
- 30 octobre: relâche
- 6 novembre (J. G.)
- Faisceaux (définitions, exemples — sans catégories)
- 13 novembre (J. G.)
- Catégories, faisceaux (suite).
- 20 novembre (J. G.)
- faisceaux, propriétés des faisceaux
- 27 novembre (J. G.)
- Espace étalé, construction du faisceau associé à un préfaisceau
- 4 décembre (Ch. R.)
- Différences entre logique classique LK et logique intuitionniste LJ
- 11 décembre (Ch. R.)
- Modèles faisceautisés pour LJ: forcing de Kripke Joyal (déf)
- 18 décembre -- 8 janvier: vacances d'hiver
- 15 janvier (Ch. R.)
- Propriétés du forcing de Kripke Joyal pour la logique intuitionniste LJ
- 22 janvier: relâche (journées Informatique Mathématique à Paris)
- 29 janvier (Ch. R.)
- Validité, complétude (idée de la preuve seulement, quitte à y revenir)
- Un exemple de formule φ de la théorie des anneaux telle que: φ soit démontrable classiquement et fausse dans un modèle faisceautisé qu'on construira (φ n'est donc pas démontrable intuitionnistiquement)
- 5 février (Boas Erez)
- Théorie des ensembles et univers d'ensembles (catégorie): historique et rappels
- 12 février (Boas Erez)
- Définition d'un topos, lien avec la théorie des ensembles usuelle: univers d'ensembles (topos bivalué avec objet des entiers naturels)
- 19 février (Boas Erez)
- Topos et faisceaux sur une topologie de Grothendiek
- 26 février relâche
- 5 mars (Boas Erez)
- Construction d'un univers d'ensembles dans lequel il existe un ensemble B de cardinalité strictement inférieure à celle des partie de N et néanmoins strictement supérieure à celle de N. (forcing, construction de Paul J. Cohen dans un cadre catégorique)
- 12 mars (Ch.R.)
- Prouvabilité: algèbres de Heyting, topologies et prétopologies de Grothendieck
- Interprétation catégorique des preuves intuitionnistes:
Catégories cartésiennes fermées (CCC)
- 17 mars (Ch.R.)
- Un cas concret: interprétation de la logique propositionnelle intuitionniste (&, ->) dans les espaces cohérents
|
Bibliographie:
- Jean-Yves GIRARD Le point aveugle — cours de logique Volumes I & II, Hermann, 2006.
- Peter T JOHNSTONE Sketches of an Elephant: A Topos Theory Compendium, Volumes I & II Oxford Logic Guides (vol. 43 & 44), Oxford University Press, 2003.
- Joachim LAMBEK & Phil SCOTT Introduction to Higher-Order Categorical Logic Cambridge studies in advanced mathematics Cambridge University Press, 1988
- Saunders MAC LANE & Ieke MOERDIJK Sheaves in geometry and logic: a first introduction to topos theory Springer University Texts, 1993
- Anne Sjerp TROELSTRA & Dirk VAN DALEN Constructivism in mathematics, Vol I & II, North-Holland, 1988.
|
|