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.