Méta : J'ai déjà fait plusieurs tentatives pour
expliquer sur ce blog ce que sont les mathématiques constructives et
comment elles fonctionnent
(notamment ici — où j'ai tenté
d'expliquer les règles de la logique intuitionniste mais en même temps
je me suis embourbé dans des explications sur ce que je devrais ou
voudrais écrire —, et ici — où j'ai
publié l'introduction / motivation d'une entrée que j'avais commencé à
écrire et qui, à cause de ça, s'est complètement embourbée). Je
considère ces tentatives comme des échecs. Une raison de cet
échec est que je n'ai pas correctement expliqué, pour commencer, de
quoi il s'agit et pourquoi on s'y intéresse. Plus tard, j'ai
participé
à un
podcast avec mes collègues Sylvie Benzoni-Gavage et David Monniaux
sur le thème mathématiques honnêtes
(l'expression vient
d'une citation
de Poincaré, qui a ensuite donné lieu à
un échange
sur Twitter), où il a été question au passage d'essayer
d'expliquer ce que sont les maths constructives ; mais là aussi, j'ai
peur de m'être très mal débrouillé quand j'ai évoqué le sujet. Je
voudrais donc faire une nouvelle tentative, en reprenant à zéro.
Comme cette tentative-ci est de nouveau en train de s'embourber (ça
fait maintenant quelque chose comme six mois que j'ai commencé à
l'écrire), je me force à en publier le début comme une entrée
autonome, où je parle un petit peu de l'histoire et des motivations,
puis je commence à développer quelques principes, quitte à ce que la
fin soit un peu abrupte.
Au moins le début de cette entrée (où je parle plus d'histoire des mathématiques que de mathématiques) devrait être très largement compréhensible, quitte à sauter quelques passages un peu plus techniques.
❦
De façon extrêmement schématique (et juste pour lancer le
sujet : ceci ne se prétend pas être une explication),
les mathématiques constructives sont des
mathématiques faites dans une logique particulière
appelée logique intuitionniste. (Les
termes constructif
et intuitionniste
sont un peu — mais
pas complètement — interchangeables.) Cette logique intuitionniste
diffère de la logique usuelle dans laquelle on fait des mathématiques
(logique classique) en ce qu'elle abandonne une règle de
raisonnement, à savoir la loi du tiers exclu,
laquelle affirme — schématiquement — que ❝si quelque chose n'est pas
faux alors ce quelque chose est vrai❞. (Ou, ce qui revient au même,
la logique intuitionniste abandonne le principe du raisonnement par
l'absurde où, pour montrer que P est vrai, on suppose « par
l'absurde » que P est faux, on aboutit à une contradiction,
et on en conclut que P devait être vrai.) La logique
intuitionniste est donc plus faible que la logique
classique : du coup, prouver quelque chose en logique intuitionniste
est plus difficile ou, si on veut, il y a moins de théorèmes (un
théorème en logique intuitionniste est encore un théorème en logique
classique, mais un théorème en logique classique n'est pas forcément
un théorème en logique intuitionniste) ; donc obtenir un résultat
« constructivement » est plus fort que l'obtenir
« classiquement », et l'étude des maths constructives consiste en
bonne partie à se demander quels résultats classiques sont encore
valables constructivement, ou, à défaut, comment on peut les démontrer
autrement, ou sinon, les reformuler, pour obtenir quelque chose de
constructif.
☞ Oui mais pourquoi donc faire ça ? Pourquoi affaiblir la
logique ? Pourquoi précisément comme ça ? Pourquoi remettre en cause
la loi du tiers exclu ? Quel est l'intérêt de la démarche ? Quelles
sont les règles du jeu ? Et pourquoi ces mots constructif
et intuitionniste
? C'est ce que je veux essayer d'expliquer
ici.
Plan :
Un (tout petit) peu d'histoire du constructivisme en mathématiques
Commençons par essayer d'expliquer comment cette notion est apparue. Qu'on me permette de faire de l'histoire des maths très schématique et simplifiée, juste pour situer un peu les choses et sans prétendre décrire complètement des positions philosophiques forcément assez complexes :
La controverse Hilbert-Brouwer
L'histoire commence au début du XXe siècle à un moment où les fondements des mathématiques commencent à se mettre en place : le monde mathématique a vu se mettre en place des approches rendant l'Analyse plus rigoureuse (Cauchy, Weierstraß, Dedekind…), l'axiomatisation de l'Arithmétique (Peano), la naissance de la théorie des ensembles (Cantor) et de l'idée que celle-ci peut servir à soutenir l'ensemble des mathématiques (Frege). Deux courants apparentés émergent en philosophie des mathématiques, le logicisme et le formalisme (voir ici pour une explication de la différence — qui ne m'intéresse pas tellement ici), qui proposent de ramener, autant que possible, la pratique mathématique à l'application de règles de déduction logique à partir d'un jeu d'axiomes (voire de pure logique dans le cas du logicisme).
Chef de file du courant formaliste, David Hilbert propose, en 1904, un programme visant à fonder les mathématiques sur une base axiomatique : au moins pour une branche donnée des mathématiques, on devrait (selon le programme de Hilbert), trouver des axiomes, formaliser ces axiomes (c'est-à-dire leur donner une forme extrêmement précise ramenant, en principe, la démonstration, à un simple jeu de manipulation de symboles), et idéalement, prouver mathématiquement que les axiomes en question permettent de démontrer ou réfuter tout énoncé syntaxiquement licite, et qu'ils ne comportent pas de contradiction. (La dernière partie de ce programme sera sérieusement mise à mal à cause des limitations posées par le théorème d'incomplétude de Gödel — voir notamment ici —, mais ce n'est pas ce qui me préoccupe ici. On dit parfois que Gödel a porté le coup de grâce au programme de Hilbert, mais il me semble, au contraire que, une fois acceptées ces limitations, le programme de Hilbert a été un grand succès et qu'il est largement admis que les mathématiques ont besoin d'axiomes et de règles de déductions claires même si, dans la pratique, les démonstrations se font généralement en langage informel.)
Hilbert accueille aussi avec enthousiasme la théorie des ensembles,
qu'il qualifie de paradis créé par Cantor
, parce qu'il permet
de rendre précises les constructions admises en la matière, et il
accepte, au passage, ses infinis de différentes tailles. (Qui font
maintenant partie des mathématiques « standard », un nouveau signe de
succès du programme de Hilbert.) Il s'oppose en cela au
courant finitiste, dans lequel s'inscrit notamment
Kronecker (selon lequel les entiers naturels ont été créés par le
bon Dieu, tout le reste est l'œuvre de l'homme
) et dans une
moindre mesure Poincaré, qui rejettent ou regardent au moins avec
soupçon les constructions infinies.
Les règles de logique admises par le programme formaliste, les
règles de la logique « classique », permettent souvent de montrer
qu'un certain objet mathématique existe sans pour autant exhiber cet
objet. Ces raisonnements prennent typiquement une forme du
style : je veux montrer qu'il existe un <machin> ; supposons
au contraire que <machin> n'existe pas : dans ce cas
<…diverses conséquences sont tirées…>, ce qui est une
contradiction : ce n'est donc pas possible, et ceci prouve que
<machin> existe
. À aucun moment le <machin>
n'est construit : il est simplement montré qu'il ne peut
pas ne pas exister : classiquement, cela revient exactement au
même qu'exister, mais cela ne permet pas d'expliciter <machin> ;
on peut donc dire que la preuve n'est pas constructive
.
Deux exemples significatifs de telles preuves non constructives (ou
considérées à l'époque comme non constructives, parce qu'en fait, tout
dépend de la manière précise dont on les formalise et/ou démontre)
sont donnés par deux théorèmes mathématiques très importants et dus,
justement, aux deux protagonistes de notre histoire. Il s'agit d'une
part
du théorème
de la base de Hilbert (1888), avec comme conséquence le fait que
les anneaux d'invariants polynomiaux (peu importe de quoi il s'agit)
sont finiment engendrés, sans que la démonstration (au moins dans sa
forme initiale) exhibe explicitement un système générateur ni ne
permette de le calculer, ce qui aurait fait dire à Paul Gordan, le
grand spécialiste des invariants, ce n'est pas des mathématiques,
c'est de la théologie
(en fait, cette phrase, comme toutes les
meilleures citations,
est probablement
apocryphe). Et d'autre part,
le théorème
du point fixe de Brouwer (c. 1910), dû au
topologiste Luitzen
Egbertus Jan Brouwer, lequel théorème affirme que toute
fonction continue d'une boule dans elle-même a un point fixe, sans que
la démonstration (au moins dans sa forme initiale) exhibe un tel point
fixe ni ne permette de le calculer.
Ces preuves non-constructives heurtent la conception philosophique de Brouwer, selon lequel prouver l'existence d'un objet ne doit pouvoir se faire qu'en construisant l'objet en question. Il est également en désaccord, plus généralement, avec l'idée formaliste de ramener les mathématiques — au moins en principe — à une application mécanique de règles logiques à partir d'axiomes : pour Brouwer, la créativité de la démarche du mathématicien ne peut pas se ramener à une application formelle de règles. Par ailleurs, Brouwer se rapproche de l'école finitiste par son scepticisme au sujet des constructions infinies arbitraires autorisées par la théorie des ensembles de Cantor (même si on ne peut pas vraiment dire que Brouwer soit un finitiste). Enfin, son intuition du continu, c'est-à-dire de la droite réelle, ne s'accorde pas vraiment avec la formalisation des nombres réels par Dedekind, mais je dois dire que je ne prétends pas vraiment comprendre ce que Brouwer pensait exactement des nombres réels (par opposition aux réinterprétations ultérieures de l'intuitionnisme). Bref, pour ces différentes raisons, Brouwer s'oppose à la philosophie formaliste défendue par Hilbert (ainsi qu'à sa cousine, le logicisme) et, une fois qu'il a obtenu un poste permanent en 1912, il développe ses propres idées auxquelles il donne le nom d'intuitionnisme.