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'est-à-dire 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 , 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.

Motivations 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 qui ne contient que des quantificateurs bornés et , est un théorème. En fait, on peut même prouver que est un théorème ou 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 si 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.

Brouwer préfère l'infini potentiel qu'il traduit positivement par de nouveaux principes de finitude Arend Heyting, , North-Holland, 1971. : 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 .

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 correspond à une preuve de ou une preuve de , et une preuve constructive de fournit un terme tel que . 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 correspond à une preuve de et une preuve de , et une preuve de transforme une preuve de en une preuve de . 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 intutionnisteCette logique est agnostique et sert de base à toutes les mathématiques constructives. Il ne faut pas la confondre avec les mathématiques intuitionnistes, une école particulière de mathématiques constructives.. Certains mathématiciens comme Brouwer, fondateur de l'intuitionnisme, étaient opposés à l'idée même de formaliser les mathématiques.

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

Concepts informels en mathématiques constructives

Déterminer si un principe n'est pas constructif 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é é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 et de 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é est accepté. De même, on peut construire un nombre réel tel que si la conjecture de Goldbach est vraie et si elle est fausse. Ainsi, le principe nous permettrait de résoudre cette conjecture ; il doit donc être rejeté à son tour..

Nombres réels 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. : on définit donc un nombre réel comme une suite de nombres rationnels telle que . On peut définir ainsi explicitement la plupart des constantes rencontrées en mathématiques, comme et .

On peut définir sur les réels une relation d'ordre stricte sur les nombres réels : on dit que s'il existe tel que . Cela permet de définir la relation de « séparation () » : si , une version plus forte de la relation de différence. On définit enfin l'égalité de deux nombres réels par , leur différence par , et la relation d'ordre large par si . 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 et , . En effet, si l'on dispose d'un nombre réel , on peut calculer toutes ses décimales à une précision arbitraire ; mais pour montrer par exemple que ou , il faudrait inspecter toutes ses décimales, ce qui est impossible en un temps fini.

La relation d'ordre strict ne vérifie pas la propriété de la trichotomie , mais vérifie la propriété plus faible de comparaison : . De plus, si la relation d'ordre large n'est pas un ordre total : n'est pas démontrable.

Intuitivement, et n'apportent que peu d'informations sur et car leurs formulations est négative, au contraire de et qui sont des informations positives, desquelles on peut définir le rang à partir duquel les développements de et diffèrent.

Analyse réelle Constructivement, toutes les fonctions réelles qu'il est possible de définir sont continues. En effet, intuitivement, pour créer une discontinuité, comme par exemple la fonction , il faudrait que 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 est continue..

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 , qui est démontrable constructivement.. Bishop et ses successeurs ont montré de nombreux théorèmes d'analyse constructive.

Ensembles et fonctions Pour Bishop, pour déterminer un ensemble., 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 , 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. entre deux ensembles est définie comme une opération qui associe à chaque élément un élément , qui en plus est extensionnelle, c'est-à-dire que . L', qui dit qu'étant donné une relation entre deux ensembles et , dit que si pour tout il existe un unique tel que , alors il existe une fonction telle que pour tout , , 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.

Différentes formalisations acceptent différentes méthodes pour construire des ensembles ; néanmoins, couramment, étant donné des ensembles et , on peut construire leur union , leur produit cartésien , l'ensemble des fonctions (munies de l'égalité définie par ), et l'ensemble des éléments de qui vérifient une propriété définie sur , donnée à l'avance. L'ensemble des parties de 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.

Différentes écoles du constructivisme

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èvesPrincipe énoncé par Andreï Markov, voir N. A. Shanin, « », , vol. 21, 1968., mais d'autres constructivistes comme Brouwer le refusent..

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

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 ;