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 en premier lieu 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. A ce titre, notre é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). Pour reprendre la terminologie de Jean-Yves Girard, il s'agit là du niveau (-1) des fondations.

L'étude de la sémantique catégorique des preuves, beaucoup utilisé poru la sémantique des langages de programmation fonctionnels typés, soit le niveau (-2) sera elle aussi étudié.

Les applications envisagées, sans exclure celles à la sémantique dela programmation, se situeront plutôt en philosophie du langage et en linguistique: sémantique de la phrase, du discours ou du dialogue, sémantique lexicale.

Documents:

• Quelques notes sur les rappels de logique

Séances:

• 2010/2011: voir ici.
• 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)
• 19 mars (Ch.R.)
  • Un cas concret: interprétation de la logique propositionnelle intuitionniste (&, ->)
• 26 mars (Ch.R.)
  • Un cas concret: interprétation de la logique propositionnelle intuitionniste (&, ->) la catégorie carétésienne fermées des espaces cohérents et fonctions stables.
• 2 avril relâche
• 9 avril (Ch.R.)
  • Sémantique des preuves dans les espaces cohérents (suite): interprétation des preuves / lambda termes.
• 16 avril (Ch.R.)
  • Sémantique des preuves dans les espaces cohérents (fin): interprétation de la quantification du second ordre propositionnel, endofoncteurs représentables
• 19 avril — 23 mai relâche (vacances, comités de sélection, cours à Vérone,...)
• 11 juin Boas Erez
  • Introduction à la logique linéaire.
• 18 juin Boas Erez
  • Introduction à la logique linéaire (suite)
  • Fin de l'école pour 2009/2010.

Bibliographie:

• Yves ANDRÉ, Topos, premier chapitre des Leçons de mathématiques contemporaines à l'IRCAM, 2009
• Pierre CARTIER, Logique, catégories et faisceaux. Séminaire Bourbaki, 20 (1977-1978), Exp. No. 513, 24 p.
• 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
• Luc ILLUSIE What is ... a topos Notices of the AMS 51(9), pp. 1060-1061, 2004.
• Saunders MAC LANE & Ieke MOERDIJK Sheaves in geometry and logic: a first introduction to topos theory Springer University Texts, 1993
• Jean PETITOT, La neige est blanche ssi... Prédication et perception Mathématiques et Sciences Humaines, 140, pp. 35-50, 1997
• Anne Sjerp TROELSTRA & Dirk VAN DALEN Constructivism in mathematics, Vol I & II, North-Holland, 1988.