Pensez à lire la Charte avant de poster !

$\newcommand{\K}{\mathbf K}$


Les-Mathematiques.net - Cours de mathématiques supérieures
 Les-Mathematiques.net - Cours de mathématiques universitaires - Forum - Cours à télécharger

A lire
Deug/Prépa
Licence
Agrégation
A télécharger
Télécharger
190 personne(s) sur le site en ce moment
E. Cartan
A lire
Articles
Math/Infos
Récréation
A télécharger
Télécharger
Théorème de Cantor-Bernstein
Théo. Sylow
Théo. Ascoli
Théo. Baire
Loi forte grd nbre
Nains magiques
 
 
 
 
 

Qu'est-ce qu'une preuve ?

Envoyé par pourexemple 
Qu'est-ce qu'une preuve ?
il y a trois années
avatar
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.



Edité 1 fois. La dernière correction date de il y a trois années et a été effectuée par jacquot.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
Tu veux la définition de la notion de preuve par un non-matheux ? Pour moi un matheux c'est quelqu'un qui a compris ce qu'était une preuve smiling smiley.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Une preuve consiste à dériver ce qui est prouvé de ce qui est supposé (les axiomes) via des règles logiques (données elles aussi).
Elle a par conséquent une structure d'arbre: à la racine le résultat prouvé, et chaque étape peut utiliser plusieurs prémisses.

Un habitant de $\varnothing$
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Ça ne ressemble pas à "un plaidoyer qui réponde à toutes les objections", quoiqu'étant donné une "objection", il y aira une étape dans la preuve (éventuellement la fin) qui montrera que l'objection est fausse.

Un habitant de $\varnothing$
Re: Qu'est-ce qu'une preuve ?
il y a trois années
Moi je suis plutôt d'accord avec 1528grinning smiley

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Je pense que par "compréhensible d'un non-matheux" contrexemple entendait "compréhensible pour quelqu'un qui est non matheux", et non pas "définition donnée par un non-matheux".
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é.

Un habitant de $\varnothing$
Re: Qu'est-ce qu'une preuve ?
il y a trois années
@L'Axone du Choix

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.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
@L'Axone: tu as peut-être raison. Dans ce cas pour moi une preuve est la donnée de : règles de déduction; axiomes; un suite de formules $(H_0,...,H_n)$ (finie) telle que tous les $H_i$ soient ou un axiome ou déduite des $H_j, j < i$ à l'aide des règles de déduction données.

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Qu'est-ce qu'une preuve ?
il y a trois années
@CE:

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 grinning smiley )

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 grinning smiley

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi ...... Cliquez sur cet implicite, pour économiser
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Merci pour vos réponses.

@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.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
PS : effectivement j'aimerais une définition qui soit comprise du plus grand nombre.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Maxtimax: oui, à condition de faire apparaître comment chaque étape est dérivée des précédentes.

Un habitant de $\varnothing$
Re: Qu'est-ce qu'une preuve ?
il y a trois années
@CE une preuve EST une stratégie infaillible. Il n'y a pas d'étage supplémentaire à monter. Avec les fresh variables elle se décrit comme un texte fini très simple (un arbre) seule l'option 2 livrant des branchements vers 2 fils.

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

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi ...... Cliquez sur cet implicite, pour économiser
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Ah bon, on peut voir qu'une stratégie est infaillible d'un simple coup d’œil ?
Bref c'est au ressenti des attaquants...

Bonne journée.



Edité 1 fois. La derni&egrave;re correction date de il y a trois ann&eacute;es et a &eacute;t&eacute; effectu&eacute;e par contrexemple.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
Oui ça se voit d'un simple coup d'œil. Ça donne un arbre dans lequel les feuilles sont des hypothèses prises le long de l'unique branche qui mène, et où les seuls branchements à 2 fils vers une P sont des fils de la forme A=>P et A. Les autres sont des branchements à un seul fils: de la forme "pour tout x R(x) donc R(a)".

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

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi ...... Cliquez sur cet implicite, pour économiser
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Alors dis moi ma stratégie est-elle infaillible ?

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

Bonne journée.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Je pense que ton truc a assez peu de chances de marcher. En effet, un critère de simplicité est la longueur d'une formule. Pour tout $n$ il y a un nombre fini de formules de longueur moins que $n$. Et il y a des formules arbitrairement "difficile à prouver" (notion à définir précisément cependant). Il en résulte que pour obtenir des formules de plus en plus difficiles à prouver on est obligé de les prendre de plus en plus complexes.

Un habitant de $\varnothing$
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Bonjour,

Je suis d'accord cela à très peu de chance de marcher, mais je crois au miracle.

Bonne journée.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
Si $\mathcal T$ est un "ensemble" d'énoncés, une preuve dans $\mathcal T$ est une suite $\mathbf A_1,...,\mathbf A_n$ d'énoncés avec pour tout $i \in \{1,...,n\}$, $\mathbf A_i \in \mathcal T$, ou bien il existe $j,k <i$ tel que $\mathbf A_j= (\mathbf A_k \implies \mathbf A_i)$ (en gros: une suite où chaque terme est obtenu soit via un modus ponens d'énoncés précédents, soit en l'invoquant comme axiome de $\mathcal T$).
Les éléments de $\mathcal T$ sont des axiomes logiques ou des énoncés plus spécifiques.
Cf également [fr.wikipedia.org]
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" ? grinning smiley)
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)

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




Edité 3 fois. La derni&egrave;re correction date de il y a trois ann&eacute;es et a &eacute;t&eacute; effectu&eacute;e par Foys.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
J'ai vraiment l'impression qu'un plaidoyer devient une preuve que si et seulement si aucun attaquant ne voit d'objection au plaidoyer.

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.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Fermat-Wiles?

Un habitant de $\varnothing$
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
C'est, me semble-t-il, plus ancien que cela, mais je ne saurais pas donner de date exacte.



Edité 1 fois. La derni&egrave;re correction date de il y a trois ann&eacute;es et a &eacute;t&eacute; effectu&eacute;e par jacquot.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
@foys: la définition que j'ai donnée est tout à fait usuelle*** même si présentée en termes de jeu. Les stratégies infaillibles sont exactement les arbres de séquents appelés "preuves" dans n'importe quel cours

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

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi ...... Cliquez sur cet implicite, pour économiser
Re: Qu'est-ce qu'une preuve ?
il y a trois années
Oui mais l'expression "stratégie infaillible" n'est pas définie; en fait il faaudrait expliquer ce qu'est une preuve pour lui donner un sens.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
Dans cas présent c'est un arbre sans branche infinie.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi ...... Cliquez sur cet implicite, pour économiser
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
J'ai déjà failli intervenir, mais la canicule aidant, je suis cloîtré chez moi.

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.

Citation
contrexemple :
J'ai vraiment l'impression qu'un plaidoyer devient une preuve que si et seulement si aucun attaquant ne voit d'objection au plaidoyer.

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

L'homme n'est ni ange ni bête, et le malheur veut que qui veut faire l'ange fait la bête.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
@Bruno de mon téléphone : je comprends ce que tu dis mais il me semble que tu n'insistes pas assez sur la séparation axiomes | connexions.

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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi ...... Cliquez sur cet implicite, pour économiser
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Je n'insistais pas sur la séparation axiomes/définitions, car je ne me focalisais pas sur le raisonnement mathématique. Quels sont les axiomes utilisés par un juriste dans ses raisonnements ?

Bruno

L'homme n'est ni ange ni bête, et le malheur veut que qui veut faire l'ange fait la bête.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
De mon téléphone : comme partout il y en plein!! Ce qui fera que son texte est une preuve ou pas c'est UNIQUEMENT qu'ils se voient : si oui c'est une preuve sinon non.

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)

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi ...... Cliquez sur cet implicite, pour économiser
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Bonjour,

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.



Edité 1 fois. La derni&egrave;re correction date de il y a trois ann&eacute;es et a &eacute;t&eacute; effectu&eacute;e par contrexemple.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
Une preuve montrant tous ses axiomes, elle montre ce que tu appelles "axiome tellement évident qu'on y croit", ça ne change rien au schmilblck et je suis d'accord avec toi que les "bons axiomes" sont une activité pertinente. Mais une seule spécialité*** s'en occupe pour l'instant, les autres se contentant d'enregistrer les informations sans même se préoccuper desdits: ils "font confiance"

*** la théorie des ensembles (au sens labos)

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi ...... Cliquez sur cet implicite, pour économiser
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Ce que tu dis n'étant pas un contrexemple, j'interprète donc ta réponse comme une confirmation partielle.
Re: Qu'est-ce qu'une preuve ?
il y a trois années
avatar
Il y a aussi la fameuse correspondance de Curry-Howard, qui a une preuve associe un programme, mais là encore comment a-t-on la preuve que le programme fait bien ce pour quoi il a été programmé.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
Citation
Bruno
je serais très inquiet de penser que la police, toute scientifique qu'elle soit, construise le dossier d'accusation sur un jeu binaire !
Dans un échange normal, quand celui qui propose la thèse $X$ décide de montrer que "c'est parce que $X$ est conséquence de $Y$ et que $Y$ est vrai", l'adversaire réticent va normalement exiger d'être convaincu de $Y \to X$ et d'être convaincu de $Y$. Dans le jeu du prouveur-sceptique seule une des deux preuves est demandée (mais laissée au choix du sceptique). Bref pour que l'affirmation soit "vraie", il faut que le prouveur ait la capacité de gagner toutes ses parties et non pas une seule.
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 grinning smiley. Bruno]



Edité 2 fois. La derni&egrave;re correction date de il y a deux ann&eacute;es et a &eacute;t&eacute; effectu&eacute;e par Bruno.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
Bonjour,

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.



Edité 3 fois. La derni&egrave;re correction date de il y a deux ann&eacute;es et a &eacute;t&eacute; effectu&eacute;e par contrexemple.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
Citation
contrexemple
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,
Non, le jeu s'arrête quand le prouveur gagne (une partie particulière).
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".
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
Citation
contrexemple :
Ensuite Foys et Bruno ont objecté par la formalisation de la preuve entreprit par Hilbert,

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

L'homme n'est ni ange ni bête, et le malheur veut que qui veut faire l'ange fait la bête.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
Je vous propose de rester en mathématique, commençons par nous entendre sur une définition (formalisable, compréhensible des non matheux, voir consensuelle) que pensez vous de celle proposée :
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.



Edité 3 fois. La derni&egrave;re correction date de il y a deux ann&eacute;es et a &eacute;t&eacute; effectu&eacute;e par jacquot.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
Ben il est temps de préciser le champs de tes méditations... Tout ce qui précède est nul et non avenu !

Bruno

L'homme n'est ni ange ni bête, et le malheur veut que qui veut faire l'ange fait la bête.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
Sans parler de l'orthographe qui me donne le cancer des yeux, cette définition est assez peu mathématique.



Edité 1 fois. La derni&egrave;re correction date de il y a deux ann&eacute;es et a &eacute;t&eacute; effectu&eacute;e par Shah d'Ock.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
@Shah d'Ock : Alors si tu veux vivre vieux évite de te relire grinning smiley

@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.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
Citation
contrexemple :
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.

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

L'homme n'est ni ange ni bête, et le malheur veut que qui veut faire l'ange fait la bête.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
Ok, prenons le fameux COQ qui est un assistant de preuve, qui a prouvé que COQ fait bien ce pourquoi il a été programmé ?

Sinon la correspondance de Curry-Howard à une démonstration formelle associe-t-elle un programme et sa preuve de programme ?



Edité 1 fois. La derni&egrave;re correction date de il y a deux ann&eacute;es et a &eacute;t&eacute; effectu&eacute;e par contrexemple.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
Non, elle ne fait pas ça, mais je ne vois pas trop ce que vient faire la correspondance de Curry-Howard ici, et encore moins la "correction" du programme correspondant à une preuve (correction vis-à-vis de quelle spécification de toute façon?).
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.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
La correspondance de Curry-Howard me permet de parler de quelques de choses de plus commun qu'une preuve formelle toute en étant équivalent.

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.



Edité 1 fois. La derni&egrave;re correction date de il y a deux ann&eacute;es et a &eacute;t&eacute; effectu&eacute;e par contrexemple.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
J'ai le sentiment que tu parles de plein de choses sans rapport les unes avec les autres ci ce n'est quelques mots en commun.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
Ok, laissons donc cette conversation en suspend, en espérant que quelqu'un qui en comprenne le sens veuille en discuter.

Bonne journée.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
La correspondance de Curry-Howard, appliquée à une preuve d'un énoncé $p$, donne un programme qui par définitions est de type $p$.
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.



Edité 1 fois. La derni&egrave;re correction date de il y a deux ann&eacute;es et a &eacute;t&eacute; effectu&eacute;e par Shah d'Ock.
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
Ah, bon on ne peut pas donner de correspondance à une preuve que l'on sait fausse ?
Re: Qu'est-ce qu'une preuve ?
il y a deux années
avatar
Non. Il n'y a pas de "fausse preuve" dans ce contexte.
Désolé,vous ne pouvez pas répondre à cette discussion, elle est fermée.
Liste des forums - Statistiques du forum

Total
Discussions: 135 495, Messages: 1 307 027, Utilisateurs: 23 679.
Notre dernier utilisateur inscrit Léa 33.


Ce forum
Discussions: 2 031, Messages: 39 468.

 

 
©Emmanuel Vieillard Baron 01-01-2001
Adresse Mail:

Inscription
Désinscription

Actuellement 16057 abonnés
Qu'est-ce que c'est ?
Taper le mot à rechercher

Mode d'emploi
En vrac

Faites connaître Les-Mathematiques.net à un ami
Curiosités
Participer
Latex et autres....
Collaborateurs
Forum

Nous contacter

Le vote Linux

WWW IMS
Cut the knot
Mac Tutor History...
Number, constant,...
Plouffe's inverter
The Prime page