David Madore's WebLog: Sur une entrée en cours d'écriture

[Index of all entries / Index de toutes les entréesLatest entries / Dernières entréesXML (RSS 1.0) • Recent comments / Commentaires récents]

↓Entry #2698 [older| permalink|newer] / ↓Entrée #2698 [précédente| permalien|suivante] ↓

(mercredi)

Sur une entrée en cours d'écriture

Métamotivations : [bon, sérieusement, je ne sais pas ce que sont des métamotivations, mais je trouve ce mot trop rigolo pour ne pas l'écrire]

J'ai commencé il y a quelques semaines à écrire une entrée de ce blog (je vais dire dans un instant à quel sujet, mais pour l'instant ce n'est pas important), et il est arrivé ce qui m'arrive trop souvent : je pars plein d'enthousiasme en me disant que je vais réussir à condenser à sa substantifique moëlle un sujet fort copieux, en même temps que le vulgariser, je me mets à taper, taper, taper, la condensation espérée n'a pas vraiment lieu, au contraire, je me rends compte qu'il faut que je parle de ceci, puis de cela, le texte que j'écris devient de plus en plus indigeste, et, pire, alors que je partais tout content de me dire que l'effort d'exposition me permettra d'y voir plus clair sur le sujet dont je parle, plus je l'écris plus je commence à en avoir marre de l'écrire, donc plus je traîne à m'y mettre, et en plus quand je m'y mets je mets tellement de temps à relire ce que j'ai déjà écrit que les progrès initialement rapides deviennent de plus en plus lent, et cette lente agonie ne prend fin que quand je décide de bouger le billet en cours d'écriture dans un fichier d'entrées inachevées qui prend de plus en plus la forme d'un cimetière, parce que sinon il bloque l'écriture de toute nouvelle entrée.

(Oui, mes phrases sont trop longues. Je sais.)

Que faire quand ce genre de choses se produit ? (C'est fréquent, et j'ai déjà dû en parler plein de fois.) Je n'ai toujours pas trouvé de réponse satisfaisante. Je peux jeter l'éponge et publier l'entrée dans son état inachevé, mais c'est un peu renoncer à toute possibilité de l'améliorer ultérieurement, ce qui me déplaît (il m'arrive bien sûr de modifier des entrées déjà publiées, mais c'est pour ajouter des petites précisions mineures : personne ne va tout relire pour ça). Je peux publier les parties qui sont à peu près présentables (ces entrées fort longues se découpant en parties et sous-parties, je peux publier, disons, le premier chapitre), mais je n'aime pas beaucoup non plus parce que je risque de vouloir quand même y faire des additions ultérieures, et aussi parce que ça rompt ma promesse implicite d'essayer autant que raisonnablement possible d'écrire des entrées indépendantes sur ce blog. (Promesse qui me semble nécessaire si je veux qu'on puisse lire l'entrée #2698 de ce blog sans avoir lu les 2697 qui ont précédé, ce que sans doute personne n'a fait, je ne suis même pas sûr de l'avoir fait moi-même.) Bon, je suis de mauvaise foi, je peux bien dire je suppose qu'on a lu <telle entrée passée>, d'ailleurs il a dû m'arriver quelques fois de le faire, mais si la partie 2 met des années à arriver, personne ne la lira parce que tout le monde aura oublié la partie 1 et que personne n'aura envie de la relire. Même vis-à-vis de moi-même, quand je publie quelque chose sur ce blog, qui est un peu l'espace de swap de mon cerveau, c'est pour me décharger mentalement en me disant que je peux l'oublier puisque je pourrai toujours me relire plus tard (et du coup je ne le fais généralement pas, justement), et ça ne marche plus vraiment si je continue à vouloir donner une suite.

Mais faute d'avoir décidé, je me dis que je peux au moins publier en avance (quitte à la recopier quand même plus tard, ce n'est pas long ce ne sera pas grave) la partie motivations de l'entrée en question. Ne serait-ce que parce que les motivations, c'est un peu comme les remerciements de thèse, c'est la seule chose que doit lire la majorité des gens ; et ici, ils ont, je crois, un intérêt autonome parce que c'est beaucoup moins technique que ce qui vient (enfin, est censé venir) après ; et je ne crois pas avoir envie de les changer plus tard, et elles ont toute leur place ici puisque, finalement, je suis en train de parler de ma motivation.

(En plus, là, j'ai été aspiré par d'autres préoccupations qui m'ont bouffé plein de temps, donc l'écriture de ce billet-ci a elle-même traîné en longueur !)

Voici donc les motivations de ce billet partiellement écrit :

Motivations et introduction générales

Il y a un certain temps, j'avais publié un billet fort mal écrit sur la logique intuitionniste et les mathématiques constructives, pour essayer d'expliquer de quoi il s'agit. J'aimerais réessayer d'en parler, mais en prenant une approche différente : dans le billet précédent (que je ne vais pas supposer que le lecteur a lu, même si ça peut aider de l'avoir au moins parcouru), j'avais mis l'accent sur les règles de la logique intuitionniste (la syntaxe, si on veut), maintenant je voudrais mettre l'accent sur les « mondes » (j'utilise ce terme de façon délibérément vague et informelle, je vais revenir là-dessus) dans lesquels la logique intuitionniste s'applique — la sémantique si on veut. Je pense en effet qu'on comprend beaucoup mieux l'intérêt de cette logique (au-delà de se dire tiens, je vais m'interdire d'appliquer le tiers exclu et voyons ce qui se passe) si on commence par avoir à l'esprit quelques situations où elle s'applique.

Comme on n'a pas besoin de savoir d'avance ce qu'est la logique intuitionniste pour comprendre ces « mondes », cela peut aider, justement, à l'approcher : de l'« intérieur » ils sont régis par la logique intuitionniste, mais de l'« extérieur » ce sont des objets mathématiques classiques (d'ailleurs manipulés régulièrement par des mathématiciens qui n'ont aucune appétence particulière pour la logique, comme les faisceaux en topologie ou géométrie algébrique). Ils forment donc un pont par lequel un mathématicien classique peut comprendre ou visualiser les objets intuitionnistes.

Mais par ailleurs, ces « mondes » sont intéressants, au-delà de l'aspect logique, pour la source de contre-exemples qu'ils fournissent : un monde dans lequel toutes les fonctions ℝ→ℝ sont continues, par exemple, ou dans lequel toutes les fonctions ℕ→ℕ sont calculables, ou dans lequel le théorème des valeurs intermédiaires ne peut pas être affirmé, ou dans lequel on ne peut pas affirmer qu'une suite croissante bornée de réels converge, cela mérite qu'on s'y intéresse même si on n'a aucun intérêt particulier pour la logique : je pense, et c'est en fait ma principale motivation pour m'y intéresser, que cela permet une meilleure compréhension des objets basiques que sont les entiers naturels, les réels, les fonctions entre eux, de comment ils sont construits et de ce qui permet de démontrer ceci ou cela. (Et en comparaison au degré de technicité nécessaire pour construire des mondes dans lesquels l'axiome du choix ne vaut pas, les constructions ici sont raisonnablement peu élaborées bien que plus dépaysantes, ce qui augmente leur intérêt pédagogique.)

J'utilise ci-dessus le mot monde, délibérément vague : disons un mot à ce sujet. En logique classique, le terme correct pour désigner un monde dans lequel vaut une théorie est celui de modèle (pour montrer qu'une théorie T n'implique pas un énoncé φ, on va construire un modèle de T ne vérifiant pas φ). Il y a plusieurs notions de modèle permettant de donner une sémantique à la logique intuitionniste : modèles de Kripke, par exemple, modèles à valeurs dans une algèbre de Heyting, ou encore topoï. Les « mondes » dont je veux parler sont, en l'occurrence, des topoï, mais je ne compte pas expliquer ce qu'est un topos en général, uniquement en donner des exemples. Pourquoi ? Pas que ce soit immensément compliqué si on connaît un peu de théorie des catégories (encore qu'il y a la subtilité qu'il y a deux sens, apparentés mais distincts, du mot topos : topos de Grothendieck [dans ce cas le pluriel est un topos, des topos] ou topoï élémentaires [dans ce cas le pluriel est un topos, des topoï], ces derniers étant plus généraux que ces premiers), mais je pense que la notion de topos ne peut être correctement comprise qu'en ayant au préalable un stock d'exemples, et il s'agit donc de commencer par là. D'autre part, je ne prétends pas énoncer de résultat de complétude. Disons un mot à ce sujet.

[Le paragraphe suivant est une digression par rapport à mon propos général. On peut le sauter sans perdre le fil.]

Quand on a une théorie logique (ce mot étant pris ici, informellement, dans un sens excessivement vague et général), lui définir une sémantique, c'est définir un tas de mondes possibles (même remarque) qui valident certains énoncés (i.e., certaines choses sont vraies dans tel ou tel de ces mondes), et la moindre des choses est que la sémantique donne raison à la théorie, c'est la partie qu'on appelle la soundness en anglais, et je ne sais pas quel mot utiliser en français (cohérence ?) : dire que la sémantique Muf est sound (sensée ?) pour la théorie Truc, c'est dire que tout ce que la théorie Truc permet de démontrer sera vérifié dans chacun des « mondes » Muf. En général, ce n'est pas difficile, c'est même souvent une évidence tellement évidente qu'on ne se fatigue pas à le dire. (Mais remarquez que les « mondes » dont je veux parler, s'ils sont sound pour la logique intuitionniste, ne le sont pas pour la logique classique, et c'est bien pour ça qu'il y aura des théorèmes des mathématiques classiques qui ne seront pas valables dans certains d'entre eux, du genre le théorème des valeurs intermédiaires.) Mais l'autre chose qu'on veut souvent (mais pas forcément) avec une sémantique, c'est qu'elle soit complète, et là ça veut dire la réciproque : dire que la sémantique Muf est complète pour la théorie Truc, c'est dire que tout ce qui est vérifié dans chacun des « mondes » Muf pourra être démontré dans la théorie Truc. En logique classique du premier ordre avec la sémantique fournie par la notion habituelle de modèle, si vous savez ce que c'est, on a effectivement complétude, et le résultat en question s'appelle le théorème de complétude de Gödel (qui affirme que, dans le contexte du calcul des prédicats du premier ordre en logique classique, si φ est vrai dans tout modèle d'une théorie T alors φ est démontrable à partir de T). La question de la mesure dans laquelle les topoï définissent une sémantique complète par rapport à la logique intuitionniste dépend crucialement de ce qu'on appelle exactement la logique intuitionniste (le problème n'étant pas les règles de déduction mais ce sur quoi on s'autorise à quantifier), et essayer d'expliquer ça, sur quoi je n'ai d'ailleurs pas les idées aussi claires que je voudrais, m'entraînerait à parler de logique d'ordre supérieur, de théorie des types et de choses dont je ne veux pas parler. Donc je vais faire complètement l'impasse sur tout ce qui concerne la complétude, et du coup il n'est pas vraiment pertinent que j'explique ce qu'est un topos, ce qui m'importe ce sont les exemples que je veux exposer et le fait qu'ils soient sound.

[Fin de la digression.]

Ce qui est intéressant à comprendre, aussi, c'est le rapport entre le point de vue « interne » et le point de vue « externe » sur les « mondes » en question : on peut soit se plonger dans un de ces « mondes », le regarder avec les lunettes « internes », auquel cas on a affaire à des ensembles dans un monde de maths intuitionnistes, ou au contraire le regarder « de l'extérieur », auquel cas on a affaire à des objets un peu plus compliqués (faisceaux, par exemple, en tout cas des objets d'une catégorie et c'est cette dernière qu'on appelle topos) mais dans un monde plus familier puisque la logique classique s'applique. Les deux points de vue se traduisent l'un l'autre (du moins, tout énoncé « interne » peut se réécrire de façon « externe », la réciproque n'est pas forcément vraie), ils s'éclairent et se complètent. Ce que je voudrais faire c'est expliquer, sur quelques exemples, comment marche cet aller-retour.

Idéalement, je voudrais faire trois ou quatre entrées de blog, indépendantes les unes des autres, pour décrire trois ou quatre « mondes » (topoï) différents qui sont les exemples fondamentaux à avoir en tête, sans doute les plus faciles à décrire et les plus éclairants pour ce qui est de se faire une intuition ou de trouver des contre-exemples. (Bien sûr, comme je ne finis pas ce que je commence, je n'écrirai sans doute pas tout ça, mais ce n'est pas une raison pour ne pas en parler.) Ce serait, dans un ordre un peu arbitraire :

  • les topos de faisceaux sur un espace topologique usuel (ceci définit un topos pour chaque espace topologique),
  • le topos des ensembles simpliciaux,
  • le gros topos de Zariski (ou plus correctement, le topos des faisceaux sur le gros site de Zariski) des anneaux commutatifs (c'est-à-dire, en fait, des schémas affines),
  • et le topos effectif.

Quelques explications sur ces choix. [Ce paragraphe aussi est une digression et on peut le sauter.] D'abord, certains pourraient râler que c'est un peu idiot : les trois premiers points ci-dessus sont tous des topos de Grothendieck, alors pourquoi ne pas définir directement ce qu'est un topos de Grothendieck, c'est-à-dire le topos des faisceaux sur une topologie de Grothendieck, et du coup décrire les trois premiers d'un même coup (ce qui n'est d'ailleurs, formellement, pas tellement plus compliqué que de définir le premier point) ; mais dire ça, c'est justement rater que mon propos n'est pas de donner des définitions générales mais des exemples éclairants. Il est beaucoup plus éclairant de se rendre compte que dans le topos des faisceaux d'ensembles sur ℝ (la droite réelle usuelle), toutes les fonctions réelles sont continues que de lire un énoncé affirmant que dans le topos des faisceaux sur une topologie de Grothendieck vérifiant <telles conditions absconse>, c'est le cas. Quand je cherche à visualiser quelque chose sur les topos, personnellement, je commence toujours par essayer de me figurer les choses sur le topos des faisceaux sur un espace topologique usuel, pas sur une topologie de Grothendieck.

Bref, le premier item ci-dessus est choisi pour sa simplicité. La personne qui me lit mais ne sait pas ce que c'est qu'un espace topologique pourra prendre un espace métrique à la place si elle sait ce que c'est que ça, ou même simplement ℝ dans la mesure où elle sait ce qu'est un ouvert de ℝ, c'est à peu près tout ce dont j'ai besoin, et ce sera déjà (le topos des faisceaux d'ensembles sur ℝ) un exemple intéressant. Le second item est choisi parce qu'il est assez différent et donc différemment éclairant, et parce que sa logique propositionnelle interne est intéressante (c'est la logique de Medvedev, que j'ai déjà définie dans cette entrée — plus précisément ici —, un fait que j'ai appris ici ; donc en quelque sorte, il s'agit de développer la jolie logique de Medvedev en un vrai monde mathématique), mais aussi, très honnêtement, parce que je me dis qu'il faut que je fasse l'effort de traiter toutes sortes d'exercices consistant à comprendre ce que sont, par exemple, les réels dans ce topos, et qu'écrire un billet de blog à ce sujet me forcerait à faire ces exercices. Le troisième item est là parce que j'ai déjà défini ce topos dans ce billet (précisément ici), sans dire que c'est un topos, et qu'il est donc intéressant de revenir dessus et de parler un peu de ce topos et de ses liens avec la géométrie algébrique (mais pour ceux qui savent déjà un peu de géométrie algébrique je renvoie à ces excellentes notes d'Ingo Blechschmidt où il commence par définir tout ce qu'il faut savoir sur la logique interne). Enfin, le quatrième item est la suite de ce billet sur la réalisabilité, et cet exemple est important justement parce qu'il ne s'agit pas d'un topos de Grothendieck (peu importe ce qu'est un topos de Grothendieck, mais les trois premiers en sont), et aussi parce qu'il valide l'énoncé fort surprenant toute fonction ℕ→ℕ est calculable au sens de Church-Turing, et du coup il a un intérêt particulier en informatique.

Et dans chaque cas, mon but n'est en aucun cas d'en faire une étude générale (au-delà de quelques propriétés basiques incontournables) mais d'expliquer, d'une part, comment faire la traduction entre le point de vue « interne » et le point de vue « externe », et d'autre part, ce que sont (dans le monde « interne ») quelques objets usuels, à commencer par les entiers naturels ou les nombres réels (de différentes sortes : de Cauchy, de Dedekind), et quelles propriétés (« internes ») ils vérifient. Du style : est-ce qu'un nombre réel qui n'est pas égal à zéro est soit strictement positif soit strictement négatif ? (une fois cette question posée dans le langage « interne », on peut la traduire de façon « externe » et cela devient une question mathématique usuelle portant, disons, sur le faisceau des fonctions réelles continues sur un espace topologique dont on peut déterminer la vérité par des méthodes extrinsèques) ; ou encore est-ce que le théorème des valeurs intermédiaires est vérifié pour les fonctions réelles continues ? (qu'il faut prendre soin d'énoncer soigneusement dans le langage « interne »).

Ce que je trouve aussi intéressant avec ces exemples, c'est qu'ils fournissent un stock assez important d'exercices que je trouve dignes d'être soulevées : le topos des ensembles simpliciaux valide-t-il le théorème des valeurs intermédiaires ? quelle condition sur un espace topologique garantit-elle que le topos des faisceaux dessus valide l'axiome de Scott ((¬¬pp) ⇒ (p∨¬p)) ⇒ (¬¬p∨¬p) (cf. cette entrée, précisément ce passage) ? comment peut-on décrire l'ensemble des suites croissantes à valeurs dans {0,1} dans le topos effectif ? quelle est l'objet des nombres réels dans le topos de Zariski ? (certaines de ces questions sont sans doute stupides, mais ce sont des exemples d'un stock illimité d'exercices auxquels il est intéressant de réfléchir).

*

Motivations et introduction à cette entrée [celle en cours d'écriture, donc, que je suis en train de recopier, et pas celle-ci]

Dans ce billet, je me propose de parler du topos des faisceaux sur un espace topologique X. Comme je l'ai dit ci-dessus, si vous ne savez pas ce qu'est un espace topologique, ou simplement si on veut commencer par un cas facile mais non trivial, l'exemple X=ℝ est déjà fort intéressant, et on peut se limiter à ça. Le but est donc de :

  • définir ce qu'est un faisceau d'ensembles sur X, et un morphisme de tels faisceaux, qui collectivement constituent le topos dont je parle,
  • expliquer ce qu'est la logique interne du topos, c'est-à-dire, ce que cela signifie que le topos valide un énoncé,
  • définir certains objets importants dans ce topos, notamment le classificateur de sous-objets (le nom donné, dans un topos, à l'ensemble des parties de {•}, je veux dire, l'ensemble des parties d'un singleton, ou ensemble des valeurs de vérité), l'objet [ensemble] des entiers naturels et l'objet [ensemble] des nombres réels,
  • et expliquer comment décoder, et déterminer la validité de, certains énoncés notables dans ce topos.

Comme je l'ai dit plus haut, le but que je me donne est d'expliquer en quoi certains topoï, et ici spécifiquement celui des faisceaux sur un ensemble, constituent un « monde » mathématique régi par les lois de la logique intuitionniste, dans lequel ils se comportent comme de simples ensembles : donc je mon approche sera un peu différente de celle qui présente usuellement les faisceaux dans le cadre, disons, de la topologie algébrique ou de la géométrie algébrique, car ici je veux insister sur le fait que, quand on chausse les lunettes « internes », les faisceaux ressemblent non pas à des espaces de fonctions mais à de bêtes ensembles. Raison pour laquelle je ne parle des images directe et inverse qu'en petits caractères (puisque je ne veux pas trop jouer à changer l'espace topologique), en revanche je définis le « faisceau des sous-faisceaux » (powersheaf) qui correspond à l'ensemble des parties, une construction qu'on ne trouvera pas évoquée chez Godement ou Grothendieck par exemple.

(Voilà, donc vous aurez peut-être la suite un jour si je réussis à finir de l'écrire ou si j'abandonne et que je publie en l'état ce qui est écrit, même inachevé.)

↑Entry #2698 [older| permalink|newer] / ↑Entrée #2698 [précédente| permalien|suivante] ↑

[Index of all entries / Index de toutes les entréesLatest entries / Dernières entréesXML (RSS 1.0) • Recent comments / Commentaires récents]