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^[1], 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.

Une partie des mathématiques peut se développer sans utiliser l'axiome de choix ou le principe du tiers exclu dans toute leur généralité. Cela ne signifie pas que toutes les instances de ces schémas sont exclues: ainsi, en général, l'axiome de choix est valide sur les ensembles finis et le tiers exclu valide pour les propositions décidables, car ces cas particuliers sont démontrables. De plus, tous les systèmes considérés vérifient le principe de non-contradiction. Par exemple, dans l'arithmétique de Heyting, il est possible de prouver que pour toute proposition ${\displaystyle P}$ qui ne contient que des quantificateurs bornés ${\displaystyle \forall x\leq t}$ et ${\displaystyle \exists x\leq t}$, ${\displaystyle P\lor \neg P}$ est un théorème. En fait, on peut même prouver que ${\displaystyle P}$ est un théorème ou ${\displaystyle \neg P}$ est un théorème. 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. L'arithmétique de Heyting ne prouve notamment pas ${\displaystyle P\lor \neg P}$ si ${\displaystyle P}$ est une proposition indépendante de l'arithmétique de Peano.

En fait, 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), il est donc possible de dire que chacun d'entre eux est ou bien la somme de nombres premiers, ou ne l'est pas.

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^{[réf. nécessaire]}.

Brouwer préfère l'infini potentiel qu'il traduit positivement par de nouveaux principes de finitude^[2] : 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 refusant le principe du tiers exclu, la logique constructiviste possède une propriété d'existence que la logique classique n'a pas : une preuve constructive de ${\displaystyle A\lor B}$ correspond à une preuve de ${\displaystyle A}$ ou une preuve de ${\displaystyle B}$, et une preuve constructive de ${\displaystyle \exists x,P(x)}$ fournit un terme ${\displaystyle t}$ tel que ${\displaystyle P(t)}$. Ainsi, la preuve de l'existence d'un objet mathématique est lié à la possibilité de sa construction. Plus généralement, les mathématiques constructives interprètent les connecteurs logiques selon l'interprétation de Brouwer-Heyting-Kolmogorov: une preuve de ${\displaystyle A\land B}$ correspond à une preuve de ${\displaystyle A}$ et une preuve de ${\displaystyle B}$, et une preuve de ${\displaystyle A\to B}$ transforme une preuve de ${\displaystyle A}$ en une preuve de ${\displaystyle B}$. En revanche, les mathématiques constructives ne nient pas forcément le tiers exclu : certaines démonstrations constructives, notamment celles valables dans BISH, sont aussi valables classiquement.

Les mathématiciens à l'origine des différents courants de mathématiques constructives travaillaient généralement informellement, c'est-à-dire sans expliciter exactement les systèmes formels qu'ils utilisaient. Les différents systèmes de mathématiques constructives ont été formalisés a posteriori comme des systèmes d'axiomes supplémentaires que l'on peut ajouter à un système de base, la logique intutionniste^[3]. Certains mathématiciens comme Brouwer, fondateur de l'intuitionnisme, étaient opposés à l'idée même de formaliser les mathématiques^{[réf. nécessaire]}.

Il était considéré comme impossible, tant par Brouwer qui était en faveur des mathématiques intuitionnistes que par Hilbert qui s'y opposait, qu'abandonner la logique classique pour utiliser une logique constructive nécessiterait de sacrifier des pans entiers des mathématiques. Pour montrer qu'il était possible de faire de l'analyse sans ses principes, Erret Bishop développa dans les années 60 l'analyse constructive, qui se passe de ces principes sans les réfuter^[4],[5].

Pour déterminer si un énoncé mathématique donné est acceptable d'un point de vue constructif, il est possible de montrer qu'il entraîne un autre principe que l'on sait devoir refuser. Par exemple, si l'énoncé ${\displaystyle \forall x,y\in \mathbb {R} ,x=y\lor x\neq y}$ était vrai, on devrait pouvoir décider de l'égalité entre nombres réels ; c'est impossible, puisqu'il faudrait l'infinité des décimales de ${\displaystyle x}$ et de ${\displaystyle y}$ pour répondre qu'ils sont égaux ; donc ce principe n'est pas accepté. Cela ne veut pas dire que la négation de ce principe, l'énoncé ${\displaystyle \neg (\forall x,y\in \mathbb {R} ,x=y\lor x\neq y)}$ est accepté. De même, on peut construire un nombre réel ${\displaystyle x}$ tel que ${\displaystyle x\leq 0}$ si la conjecture de Goldbach est vraie et ${\displaystyle x>0}$ si elle est fausse. Ainsi, le principe ${\displaystyle \forall x\in \mathbb {R} ,x\leq 0\lor x>0}$ nous permettrait de résoudre cette conjecture ; il doit donc être rejeté à son tour^[6].

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. Cette définition est également valable constructivement^[7],[5] : on définit donc un nombre réel comme une suite de nombres rationnels ${\displaystyle (u_{n})_{n\in \mathbb {N} }\in \mathbb {Q} ^{\mathbb {N} }}$ telle que ${\displaystyle \forall n\forall m,|u_{n}-u_{m}|\leq 2^{-n}+2^{-m}}$. On peut définir ainsi explicitement la plupart des constantes rencontrées en mathématiques, comme ${\displaystyle e}$ et ${\displaystyle \pi }$.

On peut définir sur les réels une relation d'ordre stricte sur les nombres réels^[7] : on dit que ${\displaystyle x<y}$ s'il existe ${\displaystyle n}$ tel que ${\displaystyle y_{n}-x_{n}>2^{2-n}}$. Cela permet de définir la relation de « séparation (en anglais : appartness) » : ${\displaystyle x\mathbin {\#} y}$ si ${\displaystyle x<y\lor y<x}$, une version plus forte de la relation ${\displaystyle \neq }$ de différence. On définit enfin l'égalité de deux nombres réels ${\displaystyle x=y}$ par ${\displaystyle \neg x\mathbin {\#} y}$, leur différence ${\displaystyle x\neq y}$ par ${\displaystyle \neg x=y}$, et la relation d'ordre large ${\displaystyle \leq }$ par ${\displaystyle x\leq y}$ si ${\displaystyle \neg y<x}$. Les réels définis en ce sens sont complets au sens de Cauchy : toutes les suites de Cauchy convergent.

L'égalité ne vérifie pas toutes les propriétés qu'on lui attribue usuellement. Ainsi, comme énoncé plus haut, elle n'est pas décidable : on ne peut pas montrer, constructivement, que pour tous nombres réels ${\displaystyle x}$ et ${\displaystyle y}$, ${\displaystyle x=y\lor x\neq y}$. En effet, si l'on dispose d'un nombre réel ${\displaystyle r}$, on peut calculer toutes ses décimales à une précision arbitraire ; mais pour montrer par exemple que ${\displaystyle r=0}$ ou ${\displaystyle r\neq 0}$, il faudrait inspecter toutes ses décimales, ce qui est impossible en un temps fini^[5].

La relation d'ordre strict ${\displaystyle <}$ ne vérifie pas la propriété de la trichotomie ${\displaystyle x<y\lor x=y\lor x>y}$, mais vérifie la propriété plus faible de comparaison : ${\displaystyle a<c\to a<b\lor b<c}$. De plus, si la relation d'ordre large n'est pas un ordre total : ${\displaystyle x\leq y\lor y\leq x}$ n'est pas démontrable^[5].

Intuitivement, ${\displaystyle x\leq y}$ et ${\displaystyle x\neq y}$ n'apportent que peu d'informations sur ${\displaystyle x}$ et ${\displaystyle y}$ car leurs formulations est négative, au contraire de ${\displaystyle x<y}$ et ${\displaystyle x\mathbin {\#} y}$ qui sont des informations positives, desquelles on peut définir le rang à partir duquel les développements de ${\displaystyle x}$ et ${\displaystyle y}$ diffèrent.

Constructivement, toutes les fonctions réelles ${\displaystyle \mathbb {R} \to \mathbb {R} }$ qu'il est possible de définir sont continues. En effet, intuitivement, pour créer une discontinuité, comme par exemple la fonction ${\displaystyle x\mapsto {\begin{cases}1&{\text{si }}x>0\\0&{\text{sinon}}\end{cases}}}$, il faudrait que ${\displaystyle x>0\lor x\leq 0}$ soit démontrable, or on a vu plus haut que ce n'était pas le cas. Certaines écoles de mathématiques constructives passent outre en ne travaillant que les fonctions continues (en fait, continues uniformément sur chaque intervalle fermé), comme Bishop. A contrario, dans ses mathématiques intuitionnistes, Brouwer pouvait démontrer que chaque fonction ${\displaystyle \mathbb {R} \to \mathbb {R} }$ est continue^[8].

Constructivement, le théorème des bornes atteintes et le théorème des valeurs intermédiaires ne sont pas démontrables. En revanche, on peut souvent remplacer le théorème des valeurs intermédiaires par la proposition ${\displaystyle \forall f\forall \varepsilon >0\exists x|f(x)|<\varepsilon }$, qui est démontrable constructivement^[9]. Bishop et ses successeurs ont montré de nombreux théorèmes d'analyse constructive.

Pour Bishop, pour déterminer un ensemble^[10], il faut donner à la fois un moyen d'identifier les éléments de l'ensemble et fournir une relation d'égalité sur cet ensemble. Dans le cas de ${\displaystyle \mathbb {R} }$, on a explicité ses éléments comme des suites de rationnels vérifiant certaines propriétés, et on a ensuite définit une relation d'égalité entre elles. Un ensemble sans relation d'égalité est nommé « préensemble ».

Une fonction^[11] ${\displaystyle X\to Y}$ entre deux ensembles est définie comme une opération qui associe à chaque élément ${\displaystyle x\in X}$ un élément ${\displaystyle f(x)\in Y}$, qui en plus est extensionnelle, c'est-à-dire que ${\displaystyle x=x'\implies f(x)=f(x')}$. L'axiome du choix unique (en), qui dit qu'étant donné une relation ${\displaystyle P}$ entre deux ensembles ${\displaystyle X}$ et ${\displaystyle Y}$, dit que si pour tout ${\displaystyle x\in X}$ il existe un unique ${\displaystyle y\in Y}$ tel que ${\displaystyle R(x,y)}$, alors il existe une fonction ${\displaystyle f:X\to Y}$ telle que pour tout ${\displaystyle x\in X}$, ${\displaystyle R(x,f(x))}$, est démontrable chez Bishop, de même que les axiomes du choix dénombrable et du choix dépendant. Néanmoins, ce dernier a été remis en cause récemment^[12],[13].

Différentes formalisations acceptent différentes méthodes pour construire des ensembles^[11] ; néanmoins, couramment, étant donné des ensembles ${\displaystyle X}$ et ${\displaystyle Y}$, on peut construire leur union ${\displaystyle X\cup Y}$, leur produit cartésien ${\displaystyle X\times Y}$, l'ensemble des fonctions ${\displaystyle X\to Y}$ (munies de l'égalité définie par ${\displaystyle f=g\iff \forall x\in X,f(x)=g(x)}$), et l'ensemble ${\displaystyle \{x\in X\mid \phi (x)\}}$ des éléments de ${\displaystyle X}$ qui vérifient une propriété ${\displaystyle \phi }$ définie sur ${\displaystyle X}$, donnée à l'avance. L'ensemble ${\displaystyle {\mathcal {P}}(X)}$ des parties de ${\displaystyle X}$ n'est pas toujours accepté : il est notamment refusé par ceux qui préfèrent des mathématiques prédicatives. Enfin, on peut rencontrer divers schémas de remplacement ou de récurrence transfinie dans la littérature.

Il existe plusieurs écoles constructivistes, qui s'entendent sur de nombreux points, notamment en général un refus de la logique classique, 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^[14], mais d'autres constructivistes comme Brouwer le refusent^[15].

Plus généralement, Troelstra et van Dalen identifient différentes écoles du constructivisme^[15] :

• Les mathématiques finitistes, qui n'acceptent que les objets concrets et finitaires, tels que les entiers naturels. Elles se placent dans des systèmes très faibles comme PRA, l'arithmétique primitive récursive ;
• Les mathématiques prédicatives, qui refusent qu'un objet puisse être défini en référence à l'ensemble auquel il appartient ; ainsi, elles refusent la définition d'un nombre réel comme borne supérieure de nombres réels, mais pas nécessairement le tiers exclu ;
• Les mathématiques constructives de Bishop « BISH » ou « BCM » (en anglais : Bishop's Constructive Mathematics), telles que présentées par exemple dans son ouvrage Foundations of Constructive Analysis^[4]. Bien que cette école ne se concentre pas sur la philosophie, Troelstra et van Dalen distinguent différents principes qui sous-tendent son œuvre : l'objet d'étude principal du mathématicien sont les entiers naturels et les calculs que l'on peut faire dessus. De plus, si l'on prouve « ${\displaystyle A}$ ou ${\displaystyle B}$ », il faut pouvoir déterminer lequel entre ${\displaystyle A}$ et ${\displaystyle B}$ est vrai. Cette propriété n'est pas vérifié dans les mathématiques classiques à cause du tiers exclu. BISH ne prend néanmoins pas position sur l'acceptation d'objets qui ne sont pas donné par des algorithmes.
• Le constructivisme russe « RUSS » ou « CRM » (mathématiques constructives récursives, en anglais : Constructive Recursive Mathematics), initié par Andreï Markov Jr. dans les années 50. Cette école considère que tous les objets mathématiques sont des algorithmes, et donc que toutes les fonctions sont calculables. Cette école se caractérise notamment par son utilisation du principe de Markov, qui assure que s'il est faux qu'un algorithme ne termine pas, alors il termine.
• L'intuitionnisme « INT », initié par Brouwer, et à sa suite Heyting. Il considère que les mathématiques sont une création de l'esprit, et autorise donc la création de suites infinies ${\displaystyle \alpha (0),\ldots ,\alpha (n),\ldots }$ par itérations : à chaque « instant », seul les ${\displaystyle n}$ premières valeurs sont définies, et le reste de la suite n'est pas encore fixé. Cela s'oppose notamment à la philosophie de l'école russe, puisque la suite ${\displaystyle \alpha }$ n'est pas nécessairement récursive. De plus, il considère qu'une proposition est vraie si on en dispose d'une preuve, et fausse si on dispose d'une preuve qu'elle entraîne une contradiction. Ainsi, on ne peut pas en général montrer le tiers exclu ${\displaystyle A\lor \neg A}$ en général, puisqu'on ne peut pas déterminer si une proposition arbitraire a une preuve ou mène à une contradiction.

Néanmoins, usuellement, seuls les mathématiques BISH, RUSS et INT sont considérées, par exemple par Bridges et Richman^[16] ou par Beeson^[17]. Dans ce cadre, les mathématiques classiques sont notées CLASS, et BISH est vue comme le dénominateur commun de RUSS, INT et CLASS, notamment par Bishop lui-même : un théorème démontré dans BISH serait accepté dans les mathématiques intuitionnistes, russes et classiques. Plus récemment, des mathématiciens comme Fred Rishman^[12] et Mike Schulman^[13] considèrent que BISH n'est pas assez minimal, notamment en raison de la validité de l'axiome du choix dénombrable dans ce cadre. Mike Schulman, sans donner de définition définitive, propose par exemple la logique intuitionniste d'ordre supérieur ou le langage interne des topos élémentaires avec un objet entier naturel.

À ses débuts Brouwer a publié des démonstrations non constructives^{[réf. nécessaire]} 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^[18] ». 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^{[réf. nécessaire]}. Cependant, tous les mathématiciens n'admettent pas que Bishop ait réussi^{[réf. souhaitée]}, 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^{[réf. souhaitée]}.

• (en) Douglas Bridges, Hajime Ishihara, Michael Rathjen et Helmut Schwichtenberg, Handbook of Constructive Mathematics, Cambridge University Press, coll. « Encyclopedia of Mathematics and its Applications », 2023, 842 p. (ISBN 978-1-316-51086-5, DOI 10.1017/9781009039888 )
• (en) Michael J. Beeson, Foundations of Constructive Mathematics : Metamathematical Studies, Springer Verlag, coll. « Ergebnisse der Mathematik und ihrer Grenzgebiete. 3. Folge / A Series of Modern Surveys in Mathematics », 1985, 466 p. (ISBN 978-3-642-68952-9, ISSN 0071-1136, e-ISSN 2197-5655, DOI 10.1007/978-3-642-68952-9 )
• (en) Anne Sjerp Troelstra et Dirk van Dalen, Constructivism in Mathematics, vol. 1, Elsevier Science, coll. « Studies in Logic and the Foundations of Mathematics » (n^o 121), 1988, 355 p. (ISBN 978-0444702661), p. 1-8

• (en) Errett Bishop, Foundations of constructive analysis, New York, Mc Graw-Hill, 1967, 392 p. (lire en ligne)
• (en) Arend Heyting, Intuitionism : An Introduction, Amsterdam, North Holland Publishing, 1966, 156 p. (lire en ligne)
• Rosalie Iemhof 2008, Intuitionism in the Philosophy of Mathematics, Stanford Encyclopedia of Philosophy, [lire en ligne].

• 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.
• 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.

• Analyse constructive
• Démonstration constructive
• Logique intuitionniste
• Finitisme
• Roger Apéry (cf. « Mathématique constructive », in Penser les mathématiques, Paris, Seuil, 1982)
• L.E.J. Brouwer (intuitionnisme)
• Yvon Gauthier (philosophie et constructivisme)
• Arend Heyting (logique intuitionniste)
• Leopold Kronecker (constructivisme)

• Portail de la logique
• Portail des mathématiques