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 [ajout : le billet sur le topos effectif est ici].
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 ((¬¬p⇒p) ⇒ (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é.)