Preuve constructive - Constructive proof

En mathématiques , une preuve constructive est une méthode de preuve qui démontre l'existence d'un objet mathématique en créant ou en fournissant une méthode pour créer l'objet. Cela contraste avec une preuve non constructive (également connue sous le nom de preuve d'existence ou théorème d'existence pure ), qui prouve l'existence d'un type particulier d'objet sans fournir d'exemple. Pour éviter toute confusion avec le concept plus fort qui suit, une telle preuve constructive est parfois appelée une preuve efficace .

Une preuve constructive peut également faire référence au concept plus fort d'une preuve valable en mathématiques constructives . Le constructivisme est une philosophie mathématique qui rejette toutes les méthodes de preuve qui impliquent l'existence d'objets qui ne sont pas explicitement construits. Cela exclut, en particulier, l'utilisation de la loi du milieu exclu , de l' axiome de l'infini et de l' axiome du choix , et induit une signification différente pour certaines terminologies (par exemple, le terme «ou» a un sens plus fort en termes constructifs mathématiques que dans le classique).

Certaines preuves non constructives montrent que si une certaine proposition est fausse, une contradiction s'ensuit; par conséquent la proposition doit être vraie ( preuve par contradiction ). Cependant, le principe de l'explosion ( ex falso quodlibet ) a été accepté dans certaines variétés de mathématiques constructives, y compris l' intuitionnisme .

Preuves constructives peuvent être considérées comme définissant mathématiques certifiés algorithmes : cette idée est explorée dans l' interprétation Brouwer-Heyting-Kolmogorov de logique constructive , la correspondance de Curry-Howard entre les preuves et les programmes, et de tels systèmes logiques comme par Martin-Löf de Type intuitionniste théorie et Thierry Coquand et Gérard Huet de calcul des constructions .

Un exemple historique

Jusqu'à la fin du 19e siècle, toutes les preuves mathématiques étaient essentiellement constructives. Les premières constructions non constructives sont apparues avec la théorie des ensembles infinis de Georg Cantor et la définition formelle des nombres réels .

La première utilisation de preuves non constructives pour résoudre des problèmes précédemment considérés semble être le théorème de base de Hilbert Nullstellensatz et Hilbert . D'un point de vue philosophique, le premier est particulièrement intéressant, car impliquant l'existence d'un objet bien spécifié.

Le Nullstellensatz peut être déclaré comme suit: Si sont polynômes en n indéterminés avec complexes coefficients, qui n'ont pas complexes communs zéros , alors il y a des polynômes tels que ${\ displaystyle f_ {1}, \ ldots, f_ {k}}$${\ displaystyle g_ {1}, \ ldots, g_ {k}}$

${\ displaystyle f_ {1} g_ {1} + \ ldots + f_ {k} g_ {k} = 1.}$

Un tel théorème d'existence non constructif fut une telle surprise pour les mathématiciens de l'époque que l'un d'eux, Paul Gordan , écrivit: "ce ne sont pas des mathématiques, c'est de la théologie ".

Vingt-cinq ans plus tard, Grete Hermann a fourni un algorithme de calcul qui n'est pas une preuve constructive au sens fort, puisqu'elle a utilisé le résultat de Hilbert. Elle a prouvé que, s'ils existent, ils peuvent être trouvés avec des diplômes inférieurs à . ${\ displaystyle g_ {1}, \ ldots, g_ {k},}$${\ displaystyle g_ {1}, \ ldots, g_ {k}}$${\ displaystyle 2 ^ {2 ^ {n}}}$

Ceci fournit un algorithme, car le problème se réduit à résoudre un système d'équations linéaires , en considérant comme inconnu le nombre fini de coefficients du ${\ displaystyle g_ {i}.}$

Exemples

Preuves non constructives

Considérons d'abord le théorème selon lequel il existe une infinité de nombres premiers . La preuve d' Euclide est constructive. Mais une manière courante de simplifier la preuve d'Euclide postule que, contrairement à l'affirmation du théorème, il n'y en a qu'un nombre fini, auquel cas il y en a un plus grand, noté n . Considérons alors le nombre n ! + 1 (1 + le produit des n premiers nombres). Soit ce nombre est premier, soit tous ses facteurs premiers sont supérieurs à n . Sans établir de nombre premier spécifique, cela prouve qu'il existe un nombre supérieur à n , contrairement au postulat original.

Considérons maintenant le théorème «il existe des nombres irrationnels et tels qui sont rationnels ». Ce théorème peut être prouvé en utilisant à la fois une preuve constructive et une preuve non constructive. ${\ displaystyle a}$${\ displaystyle b}$${\ displaystyle a ^ {b}}$

La preuve de 1953 suivante de Dov Jarden a été largement utilisée comme exemple de preuve non constructive depuis au moins 1970:

CURIOSA
339. Une simple preuve qu'une puissance d'un nombre irrationnel à un exposant irrationnel peut être rationnelle. est soit rationnel, soit irrationnel. Si c'est rationnel, notre affirmation est prouvée. Si c'est irrationnel, prouve notre affirmation.      Dov Jarden Jérusalem
${\ displaystyle {\ sqrt {2}} ^ {\ sqrt {2}}}$${\ displaystyle ({\ sqrt {2}} ^ {\ sqrt {2}}) ^ {\ sqrt {2}} = 2}$

Plus en détail:

• Rappelez-vous que c'est irrationnel et que 2 est rationnel. Considérez le nombre . Soit c'est rationnel, soit c'est irrationnel. ${\ displaystyle {\ sqrt {2}}}$ ${\ displaystyle q = {\ sqrt {2}} ^ {\ sqrt {2}}}$
• Si est rationnel, alors le théorème est vrai, avec et les deux étant . ${\ displaystyle q}$${\ displaystyle a}$${\ displaystyle b}$${\ displaystyle {\ sqrt {2}}}$
• Si est irrationnel, alors le théorème est vrai, avec l' être et l' être , puisque ${\ displaystyle q}$${\ displaystyle a}$${\ displaystyle {\ sqrt {2}} ^ {\ sqrt {2}}}$${\ displaystyle b}$${\ displaystyle {\ sqrt {2}}}$

${\ displaystyle \ left ({\ sqrt {2}} ^ {\ sqrt {2}} \ right) ^ {\ sqrt {2}} = {\ sqrt {2}} ^ {({\ sqrt {2}} \ cdot {\ sqrt {2}})} = {\ sqrt {2}} ^ {2} = 2.}$

Au fond, cette preuve n'est pas constructive parce qu'elle repose sur l'énoncé «Soit q est rationnel, soit il est irrationnel» - une instance de la loi du milieu exclu , qui n'est pas valide dans une preuve constructive. La preuve non constructive ne construit pas d'exemple a et b ; il donne simplement un certain nombre de possibilités (dans ce cas, deux possibilités qui s'excluent mutuellement) et montre que l'une d'elles - mais ne montre pas laquelle - doit donner l'exemple désiré.

Il s'avère que c'est irrationnel à cause du théorème de Gelfond – Schneider , mais ce fait n'est pas pertinent pour l'exactitude de la preuve non constructive. ${\ displaystyle {\ sqrt {2}} ^ {\ sqrt {2}}}$

Preuves constructives

Une preuve constructive du théorème ci-dessus sur les pouvoirs irrationnels des irrationnels donnerait un exemple réel, tel que:

${\ displaystyle a = {\ sqrt {2}} \ ,, \ quad b = \ log _ {2} 9 \ ,, \ quad a ^ {b} = 3 \ ,.}$

La racine carrée de 2 est irrationnelle et 3 est rationnelle. est également irrationnel: s'il était égal à , alors, par les propriétés des logarithmes , 9 ⁿ serait égal à 2 ^m , mais le premier est impair et le second est pair. ${\ displaystyle \ log _ {2} 9}$${\ displaystyle m \ over n}$

Un exemple plus substantiel est le théorème mineur du graphe . Une conséquence de ce théorème est qu'un graphe peut être tracé sur le tore si, et seulement si, aucun de ses mineurs n'appartient à un certain ensemble fini de « mineurs interdits ». Cependant, la preuve de l'existence de cet ensemble fini n'est pas constructive, et les mineurs interdits ne sont pas réellement spécifiés. Ils sont encore inconnus.

Contre-exemples brouwériens

En mathématiques constructives , une affirmation peut être réfutée en donnant un contre - exemple , comme en mathématiques classiques. Cependant, il est également possible de donner un contre-exemple brouwerien pour montrer que l'énoncé est non constructif. Ce genre de contre-exemple montre que l'énoncé implique un principe connu pour être non constructif. S'il peut être prouvé de manière constructive qu'une déclaration implique un principe qui n'est pas prouvable de manière constructive, alors la déclaration elle-même ne peut pas être prouvée de manière constructive.

Par exemple, on peut montrer qu'une déclaration particulière implique la loi du milieu exclu. Un exemple de contre-exemple brouwerien de ce type est le théorème de Diaconescu , qui montre que l' axiome complet du choix est non constructif dans les systèmes de théorie constructive des ensembles , puisque l'axiome du choix implique la loi du milieu exclu dans de tels systèmes. Le domaine des mathématiques inverses constructives développe davantage cette idée en classant divers principes en termes de «combien ils sont non constructifs», en montrant qu'ils sont équivalents à divers fragments de la loi du milieu exclu.

Brouwer a également fourni des contre-exemples «faibles». Cependant, de tels contre-exemples ne réfutent pas une déclaration; ils montrent seulement qu'à l'heure actuelle, aucune preuve constructive de l'énoncé n'est connue. Un contre-exemple faible commence par prendre un problème de mathématiques non résolu, comme la conjecture de Goldbach , qui demande si tout nombre naturel pair supérieur à 4 est la somme de deux nombres premiers. Définissez une suite a ( n ) de nombres rationnels comme suit:

${\ displaystyle a (n) = {\ begin {cases} (1/2) ^ {n} & {\ mbox {si chaque entier naturel pair dans l'intervalle}} [4, n] {\ mbox {est la somme de deux nombres premiers}}, \\ (1/2) ^ {k} & {\ mbox {if}} k {\ mbox {est le nombre naturel le moins pair de l'intervalle}} [4, n] {\ mbox { qui n'est pas la somme de deux nombres premiers}} \ end {cases}}}$

Pour chaque n , la valeur de a ( n ) peut être déterminée par une recherche exhaustive, et donc a est une séquence bien définie, de manière constructive. De plus, comme a est une suite de Cauchy avec un taux de convergence fixe, a converge vers un certain nombre réel α, selon le traitement habituel des nombres réels en mathématiques constructives.

Plusieurs faits sur le nombre réel α peuvent être prouvés de manière constructive. Cependant, sur la base de la signification différente des mots en mathématiques constructives, s'il existe une preuve constructive que «α = 0 ou α ≠ 0», cela signifierait qu'il existe une preuve constructive de la conjecture de Goldbach (dans le premier cas) ou une preuve constructive que la conjecture de Goldbach est fausse (dans ce dernier cas). Comme aucune preuve de ce type n'est connue, la déclaration citée ne doit pas non plus avoir de preuve constructive connue. Cependant, il est tout à fait possible que la conjecture de Goldbach puisse avoir une preuve constructive (comme nous ne savons pas à l'heure actuelle si elle le fait), auquel cas l'énoncé cité aurait également une preuve constructive, quoique inconnue à l'heure actuelle. La principale utilisation pratique des contre-exemples faibles est d'identifier la «dureté» d'un problème. Par exemple, le contre-exemple qui vient d'être montré montre que la déclaration citée est "au moins aussi difficile à prouver" que la conjecture de Goldbach. Les contre-exemples faibles de ce type sont souvent liés au principe limité de l'omniscience .

Voir également

• Constructivisme (philosophie des mathématiques)
• Errett Bishop - auteur du livre "Foundations of Constructive Analysis".
• Théorème d'existence § Résultats d'existence `` purs ''
• Preuves d'existence d'algorithmes non constructifs
• Méthode probabiliste

Les références

Lectures complémentaires

Liens externes

• Contre-exemples faibles de Mark van Atten, Stanford Encyclopedia of Philosophy