Un ensemble d'approches mathématiques qui exigent des constructions explicites ou des algorithmes pour témoigner les assertions d'existence et qui rejettent en général des principes non constructifs comme la loi du tiers exclu non restreinte ; les preuves doivent fournir un contenu computationnel.

Principe

L'existence équivaut à la capacité de produire un témoin ou un algorithme ; les principes logiques et axiomes de théorie des ensembles ne sont acceptés que dans la mesure où ils admettent une interprétation computationnelle ou constructive (logique intuitionniste, théorie des types, théorie constructive des ensembles).

Démonstration

Une preuve constructive de l'existence du plus grand commun diviseur donnant l'algorithme d'Euclide fournit un témoin explicite et une procédure terminante, tandis qu'une preuve classique non constructive par l'absurde qui n'affirme que l'existence serait rejetée.

Mauvaise application

Qualifier une preuve classique non constructive de constructive sans fournir de témoin algorithmique, ou supposer que tout théorème classique admet une traduction constructive simple sans modifier les définitions ou renforcer les hypothèses.

Conséquence

Donne des preuves dotées d'un contenu algorithmique, permet l'extraction de programmes et le calcul vérifié à partir de preuves, et affine souvent les énoncés classiques en formes interprétables computationnellement.

Inversion

Les mathématiques classiques traitent la vérité plus permissivement (admettent le tiers exclu et des preuves d'existence non constructives) et privilégient les énoncés de théorèmes plutôt que la fourniture de témoins, donnant des affirmations d'existence plus courtes ou plus générales au prix d'algorithmes.

Limite

Regroupe plusieurs systèmes formels (analyse constructive à la Bishop, théorie des types intuitionniste, théorie constructive des ensembles) avec des axiomes différents ; n'inclut pas la mathématique classique à moins qu'elle ne soit reformulée pour fournir des constructions.

Tension sémantique

Tension entre le désir de témoins constructifs et la commodité classique des principes non constructifs ; entre différentes écoles constructives sur les axiomes acceptables (choix, choix dénombrable, principe de Markov).

Synthèse

Les mathématiques constructives exigent de façon cohérente que les affirmations d'existence correspondent à des constructions ou algorithmes explicites, reconfigurant la logique et les fondements pour privilégier le contenu computationnel et le témoignage vérifiable en analyse, algèbre et logique.