Plusieurs démonstrations pour un théorème

or je n'ai jamais vu aucun mathématicien ou logicien se poser ou être perturbé par la question. Je me dis donc qu'il y a quelque chose qui m'échappe, que je fais une erreur de raisonnement quelque part dans mes pensées.

Peu sont perturbés, mais la question a été maintes fois posée et les réponses sont très connues: ni ton (1), ni ton (2) ne les englobe. D'ailleurs ni ton (1), ni ton (2) ne sont "corrects".

Il n'y a que des démonstrations formelles (les autres textes sont appelés "démonstrations" par abus de langage). Donc tout est précisé.

tous les théorèmes ont une infinité de démonstrations. Ca n'a rien d'extrarodinaire. On peut prouver 0=0=>0=0 en 5 000 000 000 d'étapes si on veut avec 350000000 de recours à des raisonnements par l'absurde.

Sinon, on entend parfois "démonstrations pertinentes de ce même théorème, mais profondément différentes". Bin oui ça arrive aussi et même ça arrive toujours pour tous les théorèmes. C'est juste un peu moins évident à démontrer.

Sinon, "sociologiquement", sans le faire exprès parfois les gens trouvent des preuves différentes (qu'ils auraient voulu concises) radicalement différentes d'un même théorème. Et là ils sont émus. Parce qu'ils ne l'ont pas fait exprès... Mais ça n'a rien de "spécial", puisqu'en fait tous les théorèmes sont dans cette situation.

Après il y a ce qu'on appelle des biinterprétabilité entre des théories et des langages mais c'est une autre affaire. Bien évidemment dans ce cas, comme ce ne sont pas les mêmes énoncés, les preuves sont différentes (aucune preuve de l'un n'est une preuve de l'autre puisqu'elles n'ont pas la même conclusion).

La biintrepretabilité conduit souvent aussi (mais pas toujours) à transporter les preuves.

Bonjour

est-ce que dans cette nouvelle théorie, les axiomes définis "artificiellement" démontre les axiomes d'avant

Il n'y a pas de raison pour que ce soit le cas. Mais ça n'a rien à voir avec le fait qu'il y ait deux démonstrations. Car les deux démonstrations sont parties des mêmes présupposés, et ce sont ces présupposés communs qui sont sûrs.

Je pense que tu parles trop "en général", sans t'appuyer sur une démonstration double précise (*) pour voir si tes idées ont un sens. Car il y a derrière ton discours qu'on a du mal à vraiment comprendre, une intuition non traduite complétement. Mais une intuition peut être fausse, ou à moitié fausse.

Cordialement.

(*) Par exemple deux preuves du fait que x=3 a pour conséquence x³=3x².

qu'il serait plus "propre" qu'un théorème n'ait qu'une démonstration possible parfois je me dis que c'est normal.

C'est un désir.

Mais je pense qu'il n'a pas d'autres fondements que d'exprimer la pulsion que les théorèmes sont des choses importantes et "inévitables" et je pense que cette pulsion trouve sa racine dans le fait qu'un théorème a une démonstration canonique dans la théorie dont l'ensemble des énoncés est l'ensemble des théorèmes. Auquel cas chaque théorème P a comme preuve:

1) P

avec une seule étape.

Pour te satisfaire un peu sache qu'il y a des phénomènes qui vont très légèrement dans le sens de ton désir, qui s'appellent "confluences". Ca dit en gros que si un part d'une preuve "sale" quelconque D, que l'on en élimine certaines coupures pour la rendre plus propre ou plus concrête de manières différentes en arrivant à $D_1, D_2$, alors il existe une preuve $D_3$ telle qu'on peut encore éliminer des coupures pour passer de $D_1$ à $D_3$ ainsi que pour passer de $D_2$ à $D_3$.

Comme corollaire il y a que deux preuves non réductibles $D, D'$ qui proviennent d'une même preuve "sale" $D''$ sont forcément telles que $D=D'$.

Mais attention, ne "saute" pas la dessus pour croire que ton désir serait satisfait, car ça n'a rien à voir, on doit partir d'une même preuve "sale" ou "propre".

En fait, on a même pire: tout théorème "intéressant" est un théorème qui n'a pas de preuve comment dire, "symétrique". Autrement dit, il n'existe aucun énoncé profond qui soit symétrique et qui possède une preuve symétrique.

Beaucoup de gens "naifs" ou non scientifiques expriment plus ou moins le désir contraire bien souvent "les données sont "symétriques", on devrait bien pouvoir s'en tirer en ne distinguant pas ceci et cela dans la démonstration"

Ca n'a rien d'étonnant tous ces phénomènes. L'intuition se mélange avec le désir, et bien souvent, quand on pressent une impossibilité, nait la pulsion de la réaliser (parce qu'on sent que sa réalisation => beaucoup). Et si on n'y prend garde elle peut remonter à la conscience sous forme d'une "intuition" (impression qu'un truc pourrait être "vrai") et non d'un désir (sensation des riches conséquences d'un truc, ie sensation de sa fausseté)

D'ailleurs il y a le proverbe "prendre ses désirs pour des réalités" qui ne doit pas être célèbre pour rien"

Bin, je t'ai tout dit, oui il y a peut-être un rapport entre tes idées et la confluence why not.. Mais je ne vois pas trop quoi ajouter.

Réfléchis aussi à l'intérêt d'essayer de construire un argumentaire qui in fine arriverait à la réalisation de ton désir quitte à payer le prix d'adapter des définitions. Il n'est peut-être pas énorme?

Eventuellement si tout ça t'intéresse, fais de la logique mathématique sérieusement pour voir en détails les relations entre ton idée et ce qui est connu

Turbolanding,

Pour "qu'est-ce que tu entends justement par présupposés sûr ?", il s'agit bien entendu tout simplement des hypothèses communes qu'on a avant de commencer l'une ou l'autre des démonstrations. Par exemple pour "le fait que x=3 a pour conséquence x³=3x²", les règles habituelles de calcul sur les réels, la logique classique et l'hypothèse x=3.

Cordialement.

Pour "qu'est-ce que tu entends justement par présupposés sûr ?", il s'agit bien entendu tout simplement des hypothèses communes qu'on a avant de commencer l'une ou l'autre des démonstrations

J'ai un peu la flemme de chercher dans tes posts le passage cité de toi par Gérard, mais attention, je te recommande aussi peut-être la lecture d'un de mes récents posts à samok dans le fil "raisonnement par l'absurde".

Les hypothèses et les axiomes sont placés en ce qu'on appelle des occurences négatives des énoncés scientifiques. C'est très inhabituel pour les gens souvent. Ils ont tendance à croire qu'on "croit" ou qu'on "affirme" les axiomes. Or ce n'est pas le cas. La synthèse globale d'un raisonnement (scientifique ou non d'ailleurs, tous les raisonnement précis sont scientifiques) c'est que "l'intention" finale qui apparait est que l'auteur "anonyme, abstrait" du raisonnement (un auteur "d'école en quelque sorte) a cherché à nier les axiomes en les malmenant.

Pour caricaturer: il a cherché à prouver Axiomes=>tout ***, il a raté son coup et finalement il n'a que prouvé Axiomes=>jolitruc et il est snif.

*** ("non P" est l'abréviation de P=>tout)

Méfie-toi de positionnement tels que "préjugés sûrs". Ce n'est finalement pas comme ça que fonctionne la science. C'est plutôt "il y aurait beaucoup à gagner à ce qu'on en atteste la fausseté et donc ça vaut le coup d'essayer (d'en attester la fausseté). "

A ce titre d'ailleurs, il y a eu une évolution (bon j'y connais rien en histoire des sciences, mais ça se sent) qui a conduit assez largement les gens à ne plus admettre des axiomes qui "ne rapporteraient pas beaucoup en cas de fausseté".

Un avatar de cette évolution a été l'excès et le manque de logique conduisant à des positions un peu trop radicales comme celles de Popper ou de l'ambience des physiciens actuels, les uns comme les autres, accordant un peu trop peu de cas aux démonstrations (en particulier justement au fait qu'il y en a toujours plusieurs pour un même théorème et que certains axiomes s'éliminent** ce qui fait qu'en manipulant les démonstrations comme des objets dynamiques il peut valoir le coup d'admettre un axiome dont la négation "apporterait peu" en apparence tout simplement parce qu'il est un rougage qui s'éliminera automatiquement lors d'une procédure de dépliage de la preuve. Auquel cas il valait le coup de l'admettre (puisque finalement il s'élimine et donc permet de nier les autres))

** il en va ainsi des raisonnements par l'absurde, d'axiomes de l'infini etc, bref, de tout un tas de trucs qui au premier abord peuvent apparaitre "platonicien". Un exemple "d'erreur" de cette sévérité à l'égard des axiomes trop "platoniciens" a été l'évolution de la physique à l'égard de ses problématiques quantiques: elle n'a pas assez développé "l'étude des preuves" qui sont engagées dans les "paradoxes" (qui sont des théorèmes parmi d'autres) quantiques et trop de parasites (philosphes très souvent) ont tiré les premiers en dégageant ces axiomes d'un revers de la main sans avoir réfléchi si une étude approfondie des preuves ne permettraient pas par élimination des découvertes plus précises voire vraiment importantes.
Un exemple effectif de cet accident ou de ce tort est fourni par trois dates: vers 1935 Einstein Podolsky Rosen prouve un truc qui apparait à leurs interlocuteurs comme une souris minuscule et philosphique. Il faut attendre 30 ans pour que le même raisonnement juste un peu déplié soit pris au sérieux car plus formel (connu sous "inégalités de Bell). Et encore 30 ans pour que ne soient un peu plus développé ces preuves (qui sont toujours les mêmes (via un truc connu sous le nom de GHZ par exemple). Au total, on a presque 70 ans de perdu parce qu'il y a eu une "hostilité" aux axiomes "qui apparaissaient ne pas rapporter en cas de fausseté, ie les axiomes "platoniciens d'EPR" et des réponses erronées de pseudo philosophes. )

Tu vois, c'est intéressant mais compliqué.

:S:S:S

Et je n'ai pas besoin de conseils sur le fonctionnement de la science

Euu pardon, tu as peut-être raison, mais ne le prends pas mal, je ne te répondais pas à toi du tout, je n'ai même pas lu ce que tu as dit à turboLanding (le préjugeant (ce que tu as dit, je veux dire) d'ailleurs tout à fait raisonnable à priori). C'est à lui que je m'adressais, ayant juste lu que lui avait écrit "préjugés sûrs" dans ta citation de lui

Et sinon tu as probablement raison sur ma dérive de préjugés sûrs vers "préjugés" (je pensais peut-être à tortqu'il parlait des axiomes)

Mais tu t'es encore tapé une séance où tu joues à l'expert-psychiatre ... Je veux bien croire que j'ai abordé d'autres trucs (c'est même évident), mais loool (phénomène de transfert?) toi idem avec ta psychanalyse. En plus je ne vois même pas trop ce qui peut te heurter toi dans ce que j'ai dit (à part peut-être le fait que j'évoque Popper que tu aimes bien je crois, mais bon.. c'était vrmt léger).

Sinon, oui j'ai un peu cramé un bon bout de moquette épaisse, mais faut dire que turboLanding a débarqué avec une véritable invitation à fumer même les tapis avec ce fil, du coup, je pensais que c'était la fête... Raaa, Gérard, Gérard, Gérard, qu'est-ce que tu peux être rabat-joie des fois. Pourquoi t'as pas plutôt pris un bout de moquette avec nous, tu grognes là...

-D T'inquiète Gérard et moi on est en instance de divorce en ce moment

Euu oui effectivement j'ai cru qu'il te citait, je me suis gourré.. Pardon aussi à Gérard du coup, il est normal qu'il ait cru que je lui répondais pour le coup.

christophe chalons écrivait:

---

> -D T'inquiète Gérard et moi on est en instance
> de divorce en ce moment

On va faire comme dans ce film. On dit que pendant un certain temps tu vas résoudre les exos de stats les plus imb...ables, et Gérard trivialisera les exos de TS à coup d'ultra-filtres. Ca devrait vous rapprocher. En tout cas pour Dany Boon et Sophie Marceau, ça marchait.

Perso je trouve que Sophie Marceau vieillit vraiment bien

Bah, je vois pas d'ultrafiltre sur la photo.

On peut sans doute dire qu'il y a peu d'idées en math et qu'on ne fait guère que les redécouvrir sous différents aspects. Mais ce genre de considération est d'une nature très différentes des considérations logiques qui semblent te préoccuper.

Que penses-tu des exemples suivants (j'ai essayé de chercher des exemples pas trop sophistiqués). En googlant "a new proof of " on trouve certainement des exemples plus percutants mais plus spécialisés.

- Cauchy-Scwhartz : preuves algébriques vs preuves analytiques (convexité).

- Brouwer : il y a sans doute un paquet de preuves (topologie algébrique / combinatoire / analyse complexe en dimension 2).

- Existence de fonction continues nulles part dérivables (construction explicite ; Baire ; construction du mouvement brownien).

Bon, je ne sais pas ce que ça vaut. Les spécialistes connaissent certainement un tas de trucs qu'on peut démontrer de manière probabilistes ou analytique.

Les nombres premiers doivent fournir pas mal d'exemples. Mais ce ne sont pas des preuves dans un système formel. De toutes façons, est-il possible de prouver quelque chose de consistant dans un système formel tout en restant lisible par un être humain ordinaire ? (Je veux dire, pas Sophie Marceau par exemple).

Ce que je te conseille, c'est de ne pas te contenter d'impressions, mais de travailler vraiment la question, en examinant vraiment les preuves qu'on t'a proposées. Et en essayant à leur propos, de clarifier ton "impression", pour la transformer en une constatation étayée sur des raisons sérieuses concernant les preuves.

Mais en disant "je ne fais pas "confiance" aux connaissances existantes" tu disqualifies ta démarche : ces connaissances, il ne tient qu'à toi de les acquérir. Et la suite : "je ne me résouds pas à accepter qu'il n'y a rien à chercher ou trouver puisque des gens bien plus calés y auraient déjà pensé avant moi. " n'a rien à voir avec ce qu'on t'a dit. Ce n'est pas parce que tu as une idée floue, très (trop ?) générale, pas creusée que tu as tort, mais n'est pas parce que tu as une idée floue, très (trop ?) générale que tu as découvert quelque chose. Pour passer d'une idée à une découverte, il y a toujours du travail de mise en forme. Même pour les génies ! Donc fais ce travail.

Cordialement.

turboLanding contre remarque :

oui mais j'ai déjà répondu et @turbo, sache que tu peux passer toute ta life sur cette vague question.

J'ai un peu la flemme de te prouver irréfutablement mes dires, ce sont des exos de logique.

Sinon, si tu veux en rester à des trucs pas trop formalisés, il y a une zone presque connexe entre la notion de preuve formelle et la notion "d'objets" probant (de moins en moins preuve), qui va jusqu'à, comme je te l'ai dit, mettre dans la même classe d'équivalence toutes les preuves d'un même énoncé au titre ... qu'elles démontrent le même énoncé. En regardant avec ce gros-grain les "preuves" tu auras ce que tu veux "par définition". Entre les deux il y a moult territoires à explorer

La correspondance de Curry Howard mobilise d'ailleurs probablement à elle -seule environ 300 000 euros par mois via des chercheurs pour classifier ou caractériser bien l'ensemble image de chaque telle classe** par l'application naturelle qui envoie une preuve sur un programme. Ce thème de recherche s'appelle le problème de la spécification. Ca te fait un mot-clé pour surfer sur le net et dans les BR.

**pour la relation d'équivalence p==q := "p et q prouve le même énoncé"