Qu'est-ce qu'une preuve ?
Bonjour,
Dans l'idée que j'en ai, une preuve est un plaidoyer pour une affirmation tel qu'il réponde à toutes les objections proposées, qui pourraient rendre l'affirmation fausse.
J'aimerais une définition consensuelle, compréhensible d'un non matheux, et qui soit formalisable, si cela est possible.
par ordre de priorité :
1/ formalisable
2/ compréhensible du plus grand nombre
3/ consensuelle.
Merci, par avance et bonne journée.
Dans l'idée que j'en ai, une preuve est un plaidoyer pour une affirmation tel qu'il réponde à toutes les objections proposées, qui pourraient rendre l'affirmation fausse.
J'aimerais une définition consensuelle, compréhensible d'un non matheux, et qui soit formalisable, si cela est possible.
par ordre de priorité :
1/ formalisable
2/ compréhensible du plus grand nombre
3/ consensuelle.
Merci, par avance et bonne journée.
Cette discussion a été fermée.
Réponses
Elle a par conséquent une structure d'arbre: à la racine le résultat prouvé, et chaque étape peut utiliser plusieurs prémisses.
Par ailleurs c'est fou le nombre de matheux qui n'est pas à l'aise dés que l'on se met à formaliser la logique, le raisonnement, la notion de prouvabilité versus vérité.
Effectivement, j'ai sans doute mal interprété.
"Par ailleurs c'est fou le nombre de matheux qui n'est pas à l'aise dés que l'on se met à formaliser la logique, le raisonnement, la notion de prouvabilité versus vérité."
Oui ! Mais en pratique ça n'empêche visiblement pas de faire de très bonnes maths ! Une compréhension pragmatique suffit.
Soit P une phrase et E un ensemble de phrases. Soit G le jeu suivant, qui se joue entre 2 personnes, qui démarre avec le couple $(E,P)$ (pour le confort des yeux, on préfère souvent écrire $E\vdash P$.
A chaque étape, le prouveur a plusieurs options, précisément 5 (la flèche désigne "implique"):
option1: possible seulement si $P$ est de la forme $U\to V$. Il peut dire "je prends U". Dans ce cas la partie continue avec $E\cup \{U\} \vdash V$
option2: le prouveur peut proposer une "raison"; c'est une phrase Q. Le sceptique choisit alors si on continue avec $E\vdash Q$ ou avec $E\vdash Q\to P$
option3: possible seulement si $P$ est une conjonction, ie par exemple $\forall xR(x)$. Le prouveur demande au sceptique de choisir l'objet $a$ qu'il veut et la partie continue avec $E\vdash R(a)$.
option4: la généralisation. Le prouveur peut remplacer $P$ par une phrase $Q$ dont il est évident que $P$ en est un cas particulier, par exemple, $P=R(i)$ et $Q=\forall xR(x)$. La partie continue avec $E\vdash Q$
option5: la rétro-action: le prouveur peut remplacer $P$ par une des phrases $Q$ qui était à droite du $\vdash$ dans une des positions précédentes. La partie continue avec $E\vdash Q$
Tant que la position courante $E'\vdash P'$ est telle que $P'\notin E'$, la partie continue. Sinon elle s'arrête et le prouveur gagne
$E\vdash P$ est appelé "théorème de maths" quand il existe une stratégie infaillible pour le prouveur qui démarre avec s'assure le gain de la partie. Une telle stratégie est appelée "preuve de maths".
Le caractère solitaire des activités mathématiques fait qu'on a inventé + ou - des protocoles de description exhaustives de stratégies que l'on écrit "d'un seul trait".
Le retrait de l'option5 des règles du jeu conduit à ce qu'on appelle les maths intuitionnistes
L'utilisation pragmatique de "fresh-variables" dans l'option3 permet d'avoir des preuves qui ressemblent à des textes de longueur finie (on le prouve pour $x$, et on considère qu'on l'a prouvé pour tout le monde, ie protocolé par le fameux "soit $x$" à l'école (enfin avant), maintenant c'est en L2 :-D )
On peut rajouter une contrainte: à tout moment, on est en "mode vert" ou "en mode rouge". En mode rouge, tu n'as droit qu'aux options 2,4,(5). En mode vert, tu as droit à tout. Tu passes en mode rouge dès que tu as utilisé l'option2 et quele sceptique a choisi $E\vdash Q\to P$. Et tu y restes, sauf si tu réutilises l'option2 à nouveau et que l'sceptique a la gentillesse de choisir $E\vdash Q$.
Cette contrainte qui parait pourtant très méchante est inoffensive: toute partie qui peut être gagnée sans la respecter peut être gagnée en la respectant (Ce phénomène s'appelle élimination des coupures).
Voilà, tu sais tout ce qu'un étudiant en UV m1 de logique doit savoir :-D
@CC : comment on prouve que la stratégie est infaillible ?
Faut-il juste que tous les attaquants la ressente comme infaillible ?
Ou alors faut-il une preuve qui prouve l'infaillibilité de la stratégie, et alors tu ne dis toujours pas ce qu'est une preuve.
Dessine en une tu verras peut être mieux. Je n'ai mis le protocole fresh qu'en remarque pour ne pas avoir à poster plusieurs fois des concepts proches
Bref c'est au ressenti des attaquants...
Bonne journée.
Avec la contrainte rouge vert c'est encore plus éblouissant: essentiellement c'est juste des passages d'une liste finie de choses déjà prouvées a l'une de leur conjonction.
Une conjonction de A1, A2..,An est de la forme si si A1 alors si A2 alors... alors si An alors P alors P
Sachant que j'essaie de prouver :
Que plus une conjecture est simple plus elle est dure à trouver ?
Par conjecture simple : j'entends une conjecture tellement simple qu'elle peut devenir un axiome (évidente pour tout le monde), et permettre malgré tout de faire des découvertes qui sans cela serait inenvisageable.
Je crois qu'il faut que je prenne mes cachets... :-D
Bonne journée.
Je suis d'accord cela à très peu de chance de marcher, mais je crois au miracle.
Bonne journée.
Les éléments de $\mathcal T$ sont des axiomes logiques ou des énoncés plus spécifiques.
Cf également https://fr.wikipedia.org/wiki/Système_à_la_Hilbert
Il y a de nombreux choix d'axiomes équivalents, pour la logique classique mais aussi pour les autres.
Il y a d'autres façons de définir les preuves, comme par exemple la déduction naturelle, ou encore le calcul des séquents (ces systèmes montrent -heureusement- les mêmes théorèmes).
J'ai quand même l'impression qu'un défaut du jeu du "prouveur sceptique" est que le prouveur se décharge carrément d'une partie de son job. Du reste je vois mal comment le prouveur pourrait convaincre le sceptique de sa stratégie (il lui propose une autre partie où la phrase courante est "la stragégie marche" ? :-D)
Prenons une analogie simple : le jeu d'échecs.
Une preuve que (mettons)blanc gagne est un arbre qui en fait n'existera jamais physiquement car il n'y a pas assez d'atomes dans l'univers visible pour construire le support de stockage.
Une preuve au sens du "prouveur sceptique" est ... une partie d'échecs ordinaire.
Une preuve au sens du "prouveur sceptique" de ce que blanc avait raison: c'est l'analyse après match (ce moment parfois riche en arguments de mauvaise foi et où chacun explique qu'en fait il allait gagner)
[size=x-small]"Prouveur: on va montrer l'hypothèse de Riemann. L'ensemble des présupposés est T (une théorie usuelle de maths)
Sceptique (il débute): Ok
Prouveur: je propose le choix entre "$0=0$" et $(0=0)\implies \text{Hypothèse de Riemann}$
Sceptique: euh... on va prendre $0=0$
S'ensuit une longue partie
Prouveur: Voilà, j'ai gagné, j'ai $(0=0)$ dans $T$
Sceptique: mais ..."
[/size]
En effet il y a l'exemple (je n'arrive plus à retrouver un exemple que j'avais déjà vu passer) des théorèmes que l'on pensait vrai, parce que prouvé ainsi, jusqu'à ce que l'on trouve une objection à la preuve et alors la preuve est refusée cela peut prendre plusieurs années.
[small]*** à ceci près que je remixe (mais c'est équivalent) la différence intui/classique, c'est tout, parce que je n'aime pas "ajouter" un $\perp$ gratuitement et un axiome $A\to tout\to tout\to A$ gratuitement pour une présentation ludique.[/small]
Je trouve que cette discussion a commencé sur une ambiguïté : le mot "preuve" n'est pas spécifiquement mathématique, il ne faut pas le confondre avec "démonstration" qui n'est pas non plus spécifiquement mathématique à l'exception toutefois de la démonstration "formelle" de conquête récente puisqu'elle date de la fin du XIXe siècle et qu'elle a été formulée par Hilbert (malgré les sarcasmes de Poincaré : "la logistique n'est plus stérile, elle produit des paradoxes"). Evidemment la plupart des intervenants, notamment Christophe, s'est engouffrée dans cette interprétation ! Excusez-moi, mais si par un extrême hasard, je venais à être accusé de meurtre, je serais très inquiet de penser que la police, toute scientifique qu'elle soit, construise le dossier d'accusation sur un jeu binaire !
En fait, le mot "preuve" a un sens qui dépend de l'utilisateur : un philosophe, un juriste, un homme politique, ne lui attribuent pas du tout la même valeur sémantique.
Cette preuve n'aurait de valeur que limitée dans le temps, à titre d'exemple, il y a le célèbre postulat d'Euclide dont Saccheri a donné la justification ultime car le résultat de mon étude répugnait à la nature de la ligne droite.
Second exemple : les nombres négatifs ne pouvaient pas être moindres que zéro car il ne saurait y avoir un nombre moindre que rien (Lazare Carnot).
Troisième exemple : jusqu'à Weierstrass, on pensait que toute fonction continue était $\mathcal C^1$ par morceaux puisque la dérivée formalisait une vitesse et que l'on ne concevait pas de mouvement sans vitesse.
Ceci me semble bien illustrer la fragilité de la preuve, elle est limitée par les connaissances à un instant donné ce que n'est pas la démonstration formelle.
Bruno
Certes le théorème de complétude (20ie siècle) a mis fin à l'évolution historique du type de démonstrations archivées mais j'aurais tendance à dire qu'en réalité ce qu'est une preuve n'a jamais changé au cours de l'histoire ni même d'un domaine à l'autre.
Je redonne une définition immuable de ce que veut dire le mot preuve: c'est un texte dans lequel TOUT ce qui admis se voit (et peut être facilement taggué).
Ce sont les axiomes qui changent souvent d'un domaine ou d'une époque a l'autre.On ne répétera jamais assez que ce que prouve une preuve n'est pas choisi par son auteur: c'est tours l'implication de sa conclusion par ses admis. L'espèce de mise en encre blanche d'une partie des admis par économie dlencre n'a rien à voir avec un sous entendu que ces parties non écrites seraient elles aussi justifiés. Elles restent des hypothèses pures et dures. Leur non écriture DANS LE THEOREME (dans la preuve elles se voient!) n'en fait pas des non hypothèses.
Bruno
Et ce sur quoi je voulais insister c'est que TOUTE PREUVE EST UNE PREUVE DE MATHS. Certains textes juridiques bien rédigés sont d'ailleurs plus sérieux que certains textes avachis (où les admis se voient mal) de science avérée parfois (ceci étant dû au fait qu'entre experts on est censé être capables de deviner ce que l'autre veut dire et admet sans que la syntaxe ne soit au RV)
Oui, la fameuse démonstration formelle, mais je pense qu'il existe des preuves mathématiques qui sont impossibles à formaliser, en effet je pense qu'une preuve innovante (c'est à dire une preuve que tous les lecteurs avertis s'accordent à reconnaître comme innovante) repose toujours sur une hypothèse implicite (axiome implicite) tellement évident pour les lecteurs que personnes n'en demande de justification.
Bref, selon l'idée que j'en ai les mathématiques sont un recueil de conjectures évidentes, à travers les axiomes (la face visible de l'ice-berg) et les preuves innovantes (la face invisible de l'ice-berg).
PS : désolé de caché mon ignorance derrière mon point de vue, mais celui-ci ne demande qu'une confirmation même partielle pour se renforcer, ou un contrexemple pour être reformulé, voir abandonné.
Bonne journée.
*** la théorie des ensembles (au sens labos)
Sauf que dans un procès il n'y a qu'une seule partie (et c'est la foire d'empoigne)... Le défaut de l'approche de christophe c réside plus dans ce qui précède que dans la prétendue "impossibilité métaphysique" de formaliser un raisonnement.
[Soit gentil, s'il te plaît et rends à César ce qui lui appartient :-D. Bruno]
Je rappelle que j'ai avancé la thèse suivante :
un plaidoyer devient une preuve que si et seulement si aucun attaquant ne présente d'objection au plaidoyer.
Thèse conforté par le jeu décrit par Christophe C, en effet le jeu s'arrête si le prouveur montre qu'il a une stratégie infaillible, l'infaillibilité étant du ressort du ressentie du sceptique, ce qui conforte la thèse ci-dessus.
Ensuite Foys et Bruno ont objecté par la formalisation de la preuve entreprit par Hilbert, ce à quoi j'ai répondu :
que l'on sait par la correspondance de Curry-Howard qu'une démonstration formelle peut se voir comme un programme (des termes du lambda calcul typés), or un programme ne contient pas la preuve qu'il fait bien ce pour quoi il a été programmé, et donc on revient au fait que la fiabilité du programme relève du ressenti du lecteur averti, ce qui conforte la thèse présentée.
Donc de 3 choses l'une soit j'utilise mal la correspondance de Curry-Howard, soit l'argument de la démonstration formelle va aussi dans le sens de la thèse présenté plus haut, ou enfin un cas m'a échappé.
Bonne journée.
La preuve de l'affirmation est une méthode infaillible pour gagner toutes les parties.
C'est comme si on disait, après une partie d'échecs particulière où le joueur qui a les blancs a gagné, qu'il avait "prouvé que les blancs ont une position gagnante depuis le début".
Je n'ai pas lu très attentivement ce qu'a écrit Foys, mais je ne vois pas la pertinence de la transformation de Curry Howard en ce qui concerne des preuves philosophiques par exemple.
Bruno
un plaidoyer pour une affirmation devient une preuve que(?) si et seulement si aucun attaquant avertI ne présente d'objection au plaidoyer mais aussi que tout se passe comme si l'affirmation était correcte.
Le jeu du prouveur et du sceptique ou la correspondance de Curry-Howard conforte cette définition.
@Foys : tu sembles dire que la correspondance de Curry-Howard fournie un programme et la preuve du programme, pour une démonstration formelle donnée.
Est-ce le cas ?
Sinon, le fait que le programme fasse bien ce pourquoi il a été programmé repose sur l'expertise des lecteurs avertis, du programme mais aussi sur le fait que le programme lors de ses exécutions n'est tombé sur aucun bug (qui correspond à la partie mise en gras dans la définition), ce qui confirme la proposition de définition faîtes plus haut.
Bruno
@Bruno : si on utilise la correspondance de Curry-Howard, on a la correspondance entre démonstration formelle et programme.
Or un programme est correct si les lecteurs avertis s'accorde à dire qu'il est correcte et s'il ne bug pas lors de ces exécutions.
un plaidoyer pour une affirmation devient une preuve que si et seulement si aucun attaquant averti ne présente d'objection au plaidoyer mais aussi que tout se passe comme si l'affirmation était correcte.
Ben, je connais un spécialiste d'informatique théorique qui se tordrait de rire en lisant ça ! Une preuve de programme est très délicate à établir.
Bruno
Sinon la correspondance de Curry-Howard à une démonstration formelle associe-t-elle un programme et sa preuve de programme ?
En tout cas pour l'aspect consensuel de ta définition, on repassera...
J'ai l'impression que ce qui te pose problème c'est:
"Comment savoir qu'une preuve est correcte?
-en la vérifiant algorithmiquement.
-mais comment savoir que l'algorithme est correct?
-ben, il n'a pas à être "correct" puisque c'est lui qui définit le système de preuve.
-d'accord, mais comment être certain qu'il n'y a pas eu de bug à l'exécution de l'algorithme?
-en prouvant le système qui exécute l'algorithme.
-mais comment être certain de cette preuve-là?
(...)"
Bais oui, si on n'admet pas à un moment donné qu'un système est correct, on ne peut rien "fonder" sur quelque chose de solide.
Ensuite; j'ai le souvenir d'une conférence (que je ne retrouve plus et que j'ai vu sur youtube) où un spécialiste de preuve de programme expliquait que l'on a trouvé des bugs dans des algorithmes de tris de moins d'une dizaine de ligne de codes, donc pour moi ce qui fait la fiabilité d'un programme s'est sa validation par des lecteurs avertis et surtout sa résistance au bug sur le long terme, au moins un an (point)
Après il y en aura toujours pour essayer de nous vendre des usines à gaz "prouvées" sûrs.
Désolé, pour moi, on a pas fait mieux que la bouteille de spécialistes et l'usage intensif et durable de programmes sans bugs pour prouver leurs fiabilités.
Bonne journée.
Il n'y a pas lieu de se demander si ce programme est "correct".
La correction d'un programme ne fait sens que vis-à-vis d'une spécification donnée. La seule spécification attendue d'un programme donné par la correspondance de Curry-Howard c'est d'être du bon type, mais encore une fois ça c'est automatique, c'est par définition.
Edit: je ne me ferai pas prier. Quoique je ne sois pas sûr de qui ne comprend pas quoi.