Démonstration constructive
Un article de Wikipédia, l'encyclopédie libre.
 |
Cet article est une ébauche concernant les mathématiques.
Vous pouvez partager vos connaissances en l’améliorant. (Comment ?).
|
Une première vision d'une démonstration constructive est celle d'une démonstration mathématique qui respecte les contraintes des mathématiques intuitionnistes, c'est-à-dire qui ne fait pas appel à l'infini, ni au principe du tiers exclu. Ainsi démontrer l'impossibilité de l'inexistence d'un objet ne constitue pas une démonstration constructive de son existence : il faut pour cela en exhiber un, expliquer comment le construire.
Si une démonstration est constructive, on doit pouvoir lui associer un algorithme. Cet algorithme est le contenu computationnel (ou calculatoire) de la démonstration. La correspondance de Curry-Howard énonce cette association démonstration-algorithme dans le cas des démonstrations constructives.
Une deuxième vision d'une démonstration constructive découle de la remarque précédente, c'est une démonstration à laquelle on peut donner un contenu computationnel. Des travaux récents ont montré que l'on pouvait associer (via des continuations) un contenu computationnel à la logique classique, faisant d'elle une logique constructive.
Un exemple de démonstration constructive est la démonstration du théorème de Stone-Weierstrass qui utilise les polynômes de Bernstein.
