Constructivisme (mathématiques)

En philosophie des mathématiques, le constructivisme est une position vis-à-vis des mathématiques qui considère que l'on ne peut effectivement démontrer l'existence d'objets mathématiques qu'en donnant une construction de ceux-ci, une suite d'opérations mentales qui conduit à l'évidence de l'existence de ces objets. En particulier, les constructivistes ne considèrent pas que le raisonnement par l'absurde est universellement valide, une preuve d'existence par l'absurde (c-à-d une preuve où la non-existence entraîne une contradiction) ne conduisant pas en soi à une construction de l'objet.

Le constructivisme a conduit au développement de mathématiques constructives qui suivent ces préceptes. Ainsi l'analyse constructive, développée par Errett Bishop (en), n'admet pas la propriété de la borne supérieure, car pour un constructiviste, un nombre réel est forcément engendré par une loi permettant de le calculer avec une précision arbitraire.

Le constructivisme est une position minoritaire chez les mathématiciens et les mathématiques constructives sont beaucoup moins développées que les mathématiques classiques. Le constructivisme mathématique est lié à l'intuitionnisme mathématique, sur lequel il se fonde. Il est par ailleurs possible de s'intéresser aux démonstrations constructives de certains résultats dans le cadre des mathématiques classiques.

Constructivisme et intuitionnisme

Il existe plusieurs écoles constructivistes, qui s'entendent sur de nombreux points, en particulier leurs formalisations ont pour base commune la logique intuitionniste, mais peuvent diverger sur les constructions admises pour l'existence d'un objet. Par exemple le principe de Markov est admis par ce dernier et ses élèves, mais d'autres constructivistes comme Bishop le refusent.

L'intuitionnisme de Brouwer peut être considéré comme l'une des formes du constructivisme en mathématiques qu'il a d'ailleurs inspiré, mais il y tient une place assez particulière. En général, les résultats des mathématiques constructives, celles de Bishop par exemple, sont valides du point de vue des mathématiques classiques, mais Brouwer a proposé pour les mathématiques intuitionnistes, des principes qui contredisent ces dernières, à propos du continu (la droite réelle) en particulier. Ces principes ont par exemple pour conséquence que toute fonction totale des réels dans les réels est continue. Par contre si l'on reste sur le plan strictement logique, l'intuitionnisme (au sens de la logique intuitionniste) ne démontre que des résultats valides en logique classique.

Mathématiques constructives

Les mathématiques constructives utilisent une logique constructive (plus couramment appelée logique intuitionniste), qui est essentiellement une logique classique où le principe du tiers exclu a été enlevé. Cela ne revient pas à dire que le principe du tiers exclu est complètement interdit ; des cas particuliers de ce principe seront prouvables en tant que théorèmes. Simplement, le principe n'est pas supposé en tant qu'axiome. La loi de non-contradiction, en revanche, est toujours valide.

Par exemple, dans l'arithmétique de Heyting, il est possible de prouver que pour toute proposition p qui ne contient pas de quantificateur, $\forall x,y,z,...\in \mathbb {N} :p\vee \neg p$ est un théorème (où x, y, z… sont des variables libres dans la proposition p). En ce sens, les propositions réduites à un ensemble fini peuvent toujours être vues comme étant ou vraies ou fausses, comme en mathématiques classiques, mais ce principe de bivalence n'est pas supposé pouvoir s'étendre aux propositions sur des ensembles infinis.

En fait, Luitzen Egbertus Jan Brouwer, le fondateur de l'école intuitionniste, voyait le principe du tiers exclu comme quelque chose qui était extrait de l'expérience du fini, et qui était appliqué par les mathématiciens à l'infini, sans justification. Par exemple, la conjecture de Goldbach est l'hypothèse que tout nombre pair (plus grand que 2) est la somme de deux nombres premiers. Il est possible de tester pour chaque nombre pair particulier s'il est ou non la somme de deux nombres premiers (par exemple avec une recherche exhaustive), alors il est juste de dire que chacun d'entre eux est ou bien la somme de nombres premiers, ou ne l'est pas. Et ainsi de suite, chacun d'entre eux testé jusqu'à présent est bien la somme de deux nombres premiers.

Cependant, il n'y a aucune preuve connue que la propriété est vraie pour tout nombre pair, ni aucune preuve du contraire. Ainsi, pour Brouwer, il n'est pas possible de dire « ou bien la conjecture de Goldbach est vraie, ou elle ne l'est pas ». Et indépendamment du fait que la conjecture puisse être un jour prouvée, l'argument s'applique aux problèmes similaires non résolus. Pour Brouwer, le principe du tiers exclu était équivalent à supposer que chaque problème mathématique possède une solution.

Luitzen Egbertus Jan Brouwer préfère l'infini potentiel qu'il traduit positivement par de nouveaux principes de finitude : le premier principe de Brouwer qui est un axiome d'existence et par là même inaccepté par Errett Bishop et ses disciples, le deuxième principe de Brouwer qui renforce le premier et conduit au théorème de l'éventail ou Fan Theorem.

En se séparant du principe du tiers exclu en tant qu'axiome, la logique constructiviste possède une propriété d'existence que la logique classique n'a pas : lorsque $\exists _{x\in X}P(x)$ est prouvé de manière constructive, alors $P(a)$ est prouvé de manière constructive pour au moins un $a\in X$ particulier. Ainsi, la preuve de l'existence d'un objet mathématique est lié à la possibilité de sa construction.

Exemple en analyse réelle

En analyse réelle classique, une manière de définir un nombre réel est de l'identifier à une classe de suites de Cauchy de nombres rationnels.

En mathématiques constructives, une manière de construire un nombre réel est en tant qu'une fonction $f$ prenant un entier positif $n$ et rendant un rationnel $f(n)$, en même temps qu'une fonction $g$ prenant un entier positif $n$ et rendant un entier positif $g(n)$ tel que

$\forall n:\forall i,j\geq g(n):|f(i)-f(j)|\leq {1 \over n}$

de telle sorte qu'alors la valeur $n$ augmente, les valeurs de $f(n)$ se rapprochent de plus en plus. On peut alors utiliser $f$ et $g$ ensemble pour calculer aussi précisément que souhaité une approximation rationnelle du nombre réel qu'elles représentent.

Avec cette définition, une représentation simple du nombre réel e est :

$f(n)=\sum _{i=0}^{n}{1 \over i!},\;g(n)=n$

Cette définition correspond à la définition classique en utilisant les suites de Cauchy, mais avec une touche constructive : pour une suite de Cauchy classique, il est requis que pour toute distance préalablement donnée, aussi petite soit-elle, il existe (au sens classique) un terme de la suite après lequel tous les termes sont plus proches que la distance donnée. Dans la version constructive, il est requis que pour chaque distance donnée, il soit dans les faits possible de spécifier un point de la suite où cela se produit. En fait, l'interprétation constructive standard de l'énoncé mathématique

$\forall n:\exists m:\forall i,j\geq m:|f(i)-f(j)|\leq {1 \over n}$

est précisément l'existence de la fonction calculant le module de convergence. Ainsi la différence entre les deux définitions des nombres réels peut être vue comme la différence dans l'interprétation de l'énoncé « pour tout … il existe ».

Cela pose la question de savoir quelle sorte de fonction d'un ensemble dénombrable vers un ensemble dénombrable, telle que f et g ci-dessus, peut en réalité être construite. Différentes versions du constructivisme divergent sur ce point. Les constructions peuvent être définies aussi généralement comme des séquences de choix libre : ce qui est le point de vue intuitionniste de Brouwer et Heyting, ou aussi étroitement comme des algorithmes (ou plus précisément des fonctions récursives) : point de vue de l'école constructive russe de Markov, ou même laissées non spécifiées : c'est le point de vue d'Errett Bishop. Si par exemple le point de vue algorithmique est pris, alors les réels construits ici sont essentiellement ceux qui seraient appelés de manière classique nombres réels calculables.

Attitude des mathématiciens

À ses débuts Brouwer a publié des démonstrations non constructives comme sa preuve de 1909 du théorème du point fixe de Brouwer.

Traditionnellement, les mathématiciens ont été très suspicieux, si ce n'est complètement opposés, envers les mathématiques constructives, largement en raison des limitations que cela pose pour l'analyse constructive. Ces positions ont été exprimées avec force par David Hilbert en 1928, quand il écrit dans ses Grundlagen der Mathematik, « Enlever le principe du tiers exclu aux mathématiciens serait la même chose, disons, que d'interdire le télescope aux astronomes ou aux boxeurs l'usage des poings ». Errett Bishop (en), dans son ouvrage de 1967 Foundations of Constructive Analysis, a travaillé pour dissiper ces craintes en développant une partie de l'analyse traditionnelle dans un cadre constructif. Cependant, tous les mathématiciens n'admettent pas que Bishop ait réussi, puisque son livre est nécessairement plus compliqué^{[réf. nécessaire]} qu'un livre d'analyse classique le serait.

La plupart des mathématiciens font le choix de ne pas s'astreindre à des méthodes constructives, même lorsque cela serait théoriquement possible.

Bibliographie

• Jean Largeault, L'intuitionisme, PUF, coll. « Que sais-je ? », décembre 1992.
• Collectif sous la direction de Jean Largeault, Intuitionnisme et théorie de la démonstration, Vrin, coll. Mathesis, décembre 1992.
• Pierre Ageron, Logiques, ensembles, catégories : Le point de vue constructif, Ellipses, juin 2000.
• Errett Bishop (en), Foundation of constructive analysis, Mac Graw Hill, 1967.
• Anne Sjerp Troelstra (en) et Dirk van Dalen (en), Constructivism in Mathematics, 2 volumes, collection "Studies in Logic and the Foundations of Mathematics", ed. North-Holland, 1988, (ISBN 0-444-70358-6).
• Rosalie Iemhof 2008, Intuitionism in the Philosophy of Mathematics, Stanford Encyclopedia of Philosophy, [lire en ligne].
• Jean-Michel Salanskis, Le constructivisme non standard, presses universitaires du septentrion, 1999, 349 pages. (ISBN 2-85939-604-7)
• Henri Lombardi, Épistémologie mathématique, 208 pages, éditions ellipses, 2011 (ISBN 978-2-7298-7045-4). Exposés de certains résultats classiques de mathématiques et plus particulièrement de logique mathématique menés du point de vue des mathématiques constructives.
• Henri Lombardi, Algèbre commutative, méthodes constructives: Modules projectifs de type fini, 991 pages, édition Calvage et Mounet, 2011, (ISBN 978-2-916352-21-3). Il y a aussi une seconde édition en 2016 de 1118 pages. Extrait de la préface de la seconde édition : Nous adoptons le point de vue constructif, avec lequel tous les théorèmes d’existence ont un contenu algorithmique explicite. En particulier, lorsqu'un théorème affirme l’existence d’un objet, solution d’un problème, un algorithme de construction de l’objet peut toujours être extrait de la démonstration qui est donnée
• Henri Lombardi, [PDF] Le point de vue constructif- Une introduction

Voir aussi

• Analyse constructive
• Roger Apéry (cf. « Mathématique constructive », in Penser les mathématiques, Paris, Seuil, 1982)
• Errett Bishop (en)
• L.E.J. Brouwer (intuitionnisme)
• Controverse Brouwer-Hilbert (en)
• Démonstration constructive
• Finitisme
• Yvon Gauthier (philosophie et constructivisme)
• Arend Heyting (logique intuitionniste)
• Leopold Kronecker (constructivisme)
• Logique du dialogue
• Logique intuitionniste
• Paul Lorenzen
• Andreï Markov
• Mathématiques classiques
• Henri Poincaré
• Théorie constructive des ensembles (en)
• Théorie constructive des types (en)
• Hermann Weyl