Démontrer que racine de 2 n'est pas rationnel

raoul.S · September 2020

@Chaurien toi qui es si pointilleux en ce qui concerne la langue française tu n'appliques pas la même rigueur en maths...

Au début du fil, FdP a dit (voir ICI) que la preuve classique de l’irrationalité de $\sqrt 2$ est une preuve par l'absurde. Or il se trouve que non.

PS. Pense à amo160 qui croit ce que lui a dit FdP et qui un jour tombe sur ce paragraphe de Wikipedia qui dit exactement le contraire... eh ben sa vie est fichue.

Fin de partie · September 2020

Raoul.S a écrit:

Or il se trouve que non.

Que ces preuves n'utilisent pas le principe du tiers-exclus je veux bien l'entendre mais que cela ne soit pas des preuves par l'absurde désolé vous ne m'avez pas convaincu, car dans toutes ces preuves (celles que je connais) on arrive toujours à une absurdité. Raisonnement par l'absurde, absurdité, j'ai l'impression d'avoir changé d'univers pendant mon sommeil, ou qu'on me fait une farce (un genre de diner de c.n organisé sur le forum et c'est moi qui suis le c..). 8-)
C'est comme si vous me disiez, qu'il n'y a pas de riz dans un gâteau au riz. :-D

raoul.S · September 2020

@FdP l'expression "preuve par l'absurde" est ambiguë effectivement.

Dom · September 2020

Pour moi, Fin de partie et Chaurien, vous manquez un peu d’honnêteté.

Vous dites tous les deux qu’on doit commencer par NIER l’assertion puis aboutir à une contradiction et vous ne le faites pas.
Votre première phrase de la démonstration ne contient aucune négation.

À la limite si vous écriviez quelque chose comme
« Montrons que $r$ est irrationnel.
Preuve : supposons que ce ne soit pas le cas.
C’est-à-dire que $r$ est rationnel.
$...$ » je serais d’accord avec vous. Et c’est un RPA (qu’on utilise même deux fois).

Les pros ne pourraient pas dire que vous ne faites pas un RPA. Ils pourraient éventuellement émettre d’autres critiques (oublis, raccourcis, artillerie lourde...)
Mais non, vous ne voulez pas admettre que vous commencez par quelque chose qui n’est pas une négation.
Cela m’étonne beaucoup, Chaurien.

Il ne s’agit pas du tout d’être logicien pro ou logicien amateur dans ma revendication.
C’est juste de l’ordre du français courant. Que vous revendiquez. Quel culot !

Dom · September 2020

Sur l’ambiguïté, je suis d’accord.
J’ai même trouvé un papier qui semble sérieux : http://www.logique.jussieu.fr/~alp/philomatique.pdf 109260

Fin de partie · September 2020

Dom a écrit:

Vous dites tous les deux qu’on doit commencer par NIER l’assertion puis aboutir à une contradiction et vous ne le faites pas.
Votre première phrase de la démonstration ne contient aucune négation.

Implicitement si, il y a bien une négation.
Même un étudiant en mathématiques qui n'a pas un doctorat en logique se rend compte du lien qu'il y a entre les deux assertions "$\sqrt{2}$ est rationnel" et "$\sqrt{2}$ n'est pas rationnel". Si ce n'est pas le cas, pour le coup, je vous suggère d'abandonner l'idée de lui prouver que $\sqrt{2}$ n'est pas rationnel car j'ai bien peur qu'à moins d'être amateur de diptérosodomie vous n'allez pas la-le convaincre, vous n'allez pas être compris. B-)-

PS:
Cette histoire de vraie-fausse démonstration par l'absurde est un phénomène très intéressant sociologiquement.
J'aimerais bien savoir à quelle date remonte cette fake-news. Un problème de traduction?

Dom · September 2020

Pour toi, donc : « $x$ est rationnel » contient implicitement une négation.

Rappelle-toi que tu parlais de mauvaise foi.
J’arrête avec toi.

Voyons la réponse de Chaurien, s’il souhaite répondre toutefois.

Fin de partie · September 2020

Dom: Pardon, mais pour le coup j'ai aussi eu cette vilaine pensée à ton encontre.

Supposons que $\sqrt{2}$ n'est pas irrationnel, cela ne suggère pas qu'on est en train de parler de négation?
Il faut rédiger comme ça pour le cas où on a affaire à des étudiant-e-s un peu niais-e-s qui ne savent pas qu'un nombre qui n'est pas rationnel est irrationnel et qu'un nombre qui n'est pas irrationnel est rationnel? (s'ils ne savent pas ça on peut être inquiet sur ce qu'ils vont comprendre de la démonstration qu'on souhaite dérouler devant eux)

Dom · September 2020

Ok.

Bah oui.
Il ne s’agit pas de savoir ou de ne pas savoir des « évidences ».
Il s’agit d’appliquer le cours que tu cites. Et c’est bien, c’est super même, puisque tout le monde dit la même chose sur ce cours (pro, pas pro, L1, toi, moi...).

Fin de partie · September 2020

C'est une histoire complètement dingue.
C'est exactement ce que j'écrivais au début. Un spécialiste du canis lupus familiaris bardé de diplôme constatant que les caniches ne ressemblent vraiment pas aux bergers allemands a une lubie un jour, il décide d'imposer l'idée que les caniches ne sont pas des chiens parce qu'ils ne ressemblent pas à des bergers allemands.
Comme ce type fait autorité dans son domaine personne n'ose le contredire et des tas de gens pour des raisons variées reprennent l'idée.
Quand tu leur fais remarquer qu'un caniche a les mêmes caractéristiques qu'un berger allemand ils partent dans des digressions savantes exactes sur un sujet connexe pour justifier leur jugement. Ce qu'ils ont dit est vrai, ou semble vrai et c'est censé justifier que les caniches ne sont pas des chiens devant ce savoir tu finis par douter, je ne suis qu'un béotien si DES spécialistes du canis lupus familiaris disent que le caniche n'est pas un chien ils ont sûrement raison. :-D

PS:
On est en plein conte d'Anderson, une nouvelle version des habits neufs de l'empereur.

Dom · September 2020

Tu t’égares. J’ai eu tort de continuer, je le sentais mais te trouvais raisonnable.
Je retiens l’idée d’anthologie : « $r$ est rationnel » contient implicitement une négation.
Et ça, pour toi, ce n’est pas orwellien ou kafkaien...
Bonne soirée quand même.

Blueberry · September 2020

@FdP
Je trouve que ton analogie avec les chiens n'est pas exacte.
Je dirais plutôt que tu es un peu le mec qui appellerait "chiens" les quadrupèdes qui sont vraiment des chiens mais aussi les renards.

Nous on vient te voir et on te dit :
"attention, dans ce que tu appelles chien il y a effectivement ce qu'on appelle les chiens mais il y a aussi une partie qui sont un peu différents et qu'on appelle ''renard'' "
Toi tu réponds
"Oh vous m'emm... avec vos subtilités ! Moi, tout ça, je continuerai à appeler ça ''chiens" !!''

flipflop · September 2020

@CC :

J'ai essayé ton petit exercice dans le post ici et bien je n'y suis pas arrivé sans le tiers exclu ...

Fin de partie · September 2020

Blueberry:
Toutes les analogies ne sont pas parfaites.
Quand des choses se ressemblent et qu'on les range dans la même catégorie à laquelle on a donné un nom si on veut mettre en lumière leur différences pourquoi supprimer la catégorie, et donc de taire leur ressemblances, ce serait plus pertinent de créer des sous-catégories avec chacune un nom si elle n'en ont pas déjà un.
Une ressemblance, même si vous la considérez comme grossière, est une ressemblance.

flipflop · September 2020

@Side : Pour la triple négation :

$$
((( A \to \bot) \to \bot ) \to \bot) \to ( A \to\bot)
$$
On suppose : $ H_1 := ((( A \to \bot) \to \bot) \to \bot)$ et on veut prouver que $A \to \bot$, on suppose $A$ et on doit prouver $\bot$. On applique $H_1$ et on doit prouver que $( A \to \bot) \to \bot $, on suppose $ H_2 := ( A \to \bot)$ et on doit prouver $\bot$, on applique $H_2$ et on doit prouver $A$ ce qui est un hypothèse.

Pour la réciproque :
$$
( A \to\bot) \to ((( A \to \bot) \to \bot ) \to \bot)
$$
ON suppose $( A \to\bot)$, et on veut prouver $(( A \to \bot) \to \bot ) \to \bot$, on suppose : $ H = ( A \to \bot) \to \bot $ et on veut prouver $\bot$. ON applique $H$, et on veut prouver $ A \to \bot$ c'est la première hypothèse.

Normalement, c'est ok mais vérifie !

side · September 2020

supp

side · September 2020

supp

flipflop · September 2020

@Side : le $\bot$ c'est pour dire faux et le $\to$ c'est juste une implication.

gai requin · September 2020

@flipflop : On peut prouver $\neg(\neg A\wedge\neg(\neg A))$.

flipflop · September 2020

Oui gai requin, Je suis d'accord : $ \lambda a, a_\text{right} (a_\text{left}) $ :-D

gai requin · September 2020

Et avec ça, t'as l'exo de cc. ;-)

christophe c · September 2020

De mon téléphone @side et flipflop:

Il y a équivalence entre:

A=>B

et

((A=>B)=>B)=>B

de manière générale.

Je latexifierai demain.

flipflop · September 2020

Yes je viens de voir une loi de Morgan ! Merci !

df · September 2020

J’ai l’impression que le « mathématicien classique » éprouve quelques réticences à rentrer dans le jeu tordu de la logique intuitionniste qu’il considère comme une activité périphérique !
Dans une interview à la Revue de Mathématiques Spéciales, Jean-Pierre Serre parle avec mépris de « ceux qui font joujou avec des axiomes et leurs relations logiques ».
Lui qui, de son propre aveu, a dû attendre sa soixante-dixième année pour obtenir un résultat significatif en théorie des groupes, l’a exprimé dans un cadre logique minimal.

Je mets en lien un article très éclairant sur la logique intuitionniste.
On y trouve un passage sur lequel s’accordent mathématiciens, logiciens et physiciens: il faut qu’un nombre réel soit positif ou négatif ou nul. Il ne peut pas être aucun des trois !
Cette trivialité cesse d’en être une quand on considère des éléments infinitésimaux comme $dx^2$.
...

Fin de partie · September 2020

Df a écrit:

On y trouve un passage sur lequel s’accordent mathématiciens, logiciens et physiciens: il faut qu’un nombre réel soit positif ou négatif ou nul. Il ne peut pas être aucun des trois !

Dans une preuve que $x^2=0=>x=0$ si on prend la contraposée on se retrouve avec $x\neq 0=>x^2\neq 0$ j'ai eu la nette impression que certains avaient une objection à, $x\neq 0=>x>0 \text{ ou }x<0$

Dom · September 2020

Avec des implicites que le lecteur doit deviner, tout est possible.
Certains pensent certainement que « $x=0$ contient implicitement une négation ».

Chaurien · September 2020

Juste une référence sérieuse et de bon sens :
https://artofproblemsolving.com/wiki/index.php/Proof_by_contradiction

Dom · September 2020

Chaurien,

Je remarque ton silence radio sur ce qui m’apparaît comme des contradictions.

Je te remercie cependant pour qualifier de sérieux ce papier.
Je suis une bille en anglais mais j’ai l’impression que ça parle de « réduction par l’absurde » et donc on démarre la preuve sans supposer la négation de l’assertion.
J’ai mis un extrait d’un papier (en français) qui dit clairement ces choses là, dans un message, un peu plus haut.
Mais il qualifie de « détour par l’absurde » ce qu’ici on a appelé « raisonnement par l’absurde ».
Ce papier anglais valide donc la thèse que je défends et ne valide pas la tienne.

Penses-tu comme Fin de partie que « $r$ est rationnel » contient implicitement une négation ?

Je suis d’accord pour dire que « démonstration par l’absurde » est très ambigu, compte tenu du terme « absurde » qui ne suffit pas à qualifier la preuve.

C’est dingue comme l’attachement à des principes est à géométrie variable...

claude quitté · September 2020

@Dom

Merci pour avoir pointé le texte d'Alain Prouté. Je l'ai lu plusieurs fois et je dois encore le relire. Je suis particulièrement sensible à plusieurs aspects : ``négation'', "point de vue constructif'', ``informatique'' ...etc... Peut-être le sais tu mais je me suis beaucoup intéressé, et je m'intéresse encore, à la thématique ``Que peut-on calculer en algèbre commutative et comment ?''.

Quelques remarques et questions.

0. A propos de négation. ll m'est arrivé plusieurs fois sur ce forum d'insister sur le fait d'utiliser le moins possible de négations générales (en algèbre commutative). Fort possible que je ne sois pas compris.

1. Pourquoi n'as tu pas pointé le texte de Prouté plus tôt dans ce fil ?

2. Tu termines ton fil http://www.les-mathematiques.net/phorum/read.php?3,2089942,2091230#msg-2091230 en faisant, à propos de mon extrait de Bourbaki dans mon post http://www.les-mathematiques.net/phorum/read.php?3,2089942,2090892#msg-2090892 la remarque suivante ``L’extrait de Bourbaki, est d’ailleurs fautif pour moi. Je ne vois pas noir sur blanc ce qui est nié''. Effectivement, il y aurait bien quelque chose à dire sur la dernière ligne de leur preuve. Et d'ailleurs, à mon goût, on ne voit pas assez bien où intervient le fait que les polynômes $g,h$ sont unitaires !! C'est relativement rare chez ces auteurs que tout ne soit pas écrit noir sur blanc.

Dom · September 2020

Claude,

Étant vraiment débutant en la matière (ce n’est pas de la fausse modestie), je l’ai trouvé sur Google le jour où je l’ai posté. Peut-être l’avais-je croisé jadis, toujours au sujet de ce thème.

Édit :
dans le Bourbaki de ce fil on lit « montrons par l’absurde »
dans le Bourbaki que tu postes dans l’autre fil on lit « raisonnons par l’absurde » et il commence proprement par nier.
Ça m’interpelle.
J’attends qu’on vienne me tirer les oreilles sur les spécificités françaises.
Plus sérieusement, j’attends la source « sérieuse » anglaise qui présente ce qu’est « reducto ad absurdum ».

Fin de partie · September 2020

Dom:
Tu déformes mon propos quelque peu en isolant ce qui te permet de le discréditer.
A nouveau, on est face à la situation , on veut démontrer la proposition $P$.
Et dans le texte de la démonstration figure implicitement, (explicitement éventuellement cela peut reposer sur la formulation en Français), Supposons non(${P}$)
Dans le même texte est considéré, $P$ et non(${P}$).
Toi, tu prétends si je t'ai bien compris, que parce qu'il n'y a pas explicitement écrit, non-truc, alors il n'y a pas de négation, un peu comme si sous prétexte qu'on n'a pas appelé un berger allemand rex, ou satan cela permettait de dire que cet animal n'est pas un berger allemand.
Par ailleurs, si j'ai bien compris sur une partie du fond du problème qui nous oppose tu es incohérent avec toi-même d'une certaine façon.
Si j'ai bien compris, des logiciens réunis en conclave nous donnent leur bénédiction, on n'a pas besoin d'invoquer quoi que ce soit (autre qu'une définition) pour pouvoir affirmer qu'un nombre qui n'est pas irrationnel est rationnel si un nombre irrationnel a pour définition d'être un nombre qui n'est pas rationnel, donc si j'ai toujours bien compris, on a pour la proposition $P$:"$r$ est rationnel", gratuitement sans vendre son âme au tiers-exclus ou à une autre entité démoniaque tapie dans le champ de la logique, que $non(non(P)$ est équivalente à $P$.

PS:
Après pourquoi certains parce que dans ce qu'on "vend" il n'y pas un bout de tiers-exclus certains ont décidé de retirer la licence "preuve par l'absurde" à d'autres "produits" qui sont bien des preuves et dans lequel il y a aussi de l'absurde, c'est un mystère.

Foys · September 2020

Chaurien a écrit:

Juste une référence sérieuse et de bon sens :
[artofproblemsolving.com]

Sur ces sujets les gens sans formation logique ne sont pas fiables même s'ils ont d'autres qualités.

Voilà une référence VRAIMENT sérieuse: une preuve dudit résultat dans un logiciel de vérification de preuve n'admettant pas le raisonnement par l'absurde (sauf si on l'ajoute explicitement ce qui n'est pas fait ici).

Il traîne sur mon disque; il me semble que je l'avais déjà posté sur ce forum?

(*le présent code est une preuve qu'il n'existe pas de couple d'entiers p,q avec
p non nuls, tels que p*p=2*q*q. Il compile avec COQ 8.7 et n'utilise aucun axiome additionnel 
et que des outils élémentaires (pas de librairie). 
En particulier ladite preuve se transpose sans rien changer dans l'arithmétique 
de Heyting (i.e. l'arithmétique de Peano sans raisonnement par l'absurde) *)

Lemma p_comm: forall a b:nat, a+b=b+a.
Proof.
induction a.
induction b.
reflexivity.
simpl.
rewrite <- IHb.
simpl.
reflexivity.
intros.
rewrite plus_Sn_m.
rewrite <- plus_n_Sm.
rewrite IHa.
reflexivity.
Qed.

Lemma p_asso: forall a b c:nat, a+(b+c)=(a+b)+c.
Proof.
induction a.
intros.
simpl.
reflexivity.
intros.
simpl.
rewrite IHa.
reflexivity.
Qed.

(* Certes il y a un prix à payer pour ne pas utiliser les librairies 
disponibles qui est d'avoir à démontrer un certain nombre de trivialités avant
d'avoir le résultat cible. Mais ici c'est pour montrer qu'on peut faire la 
preuve de sqrt é irrationnel à partir de quasi-rien. Dans un usage normal 
il faut évidemment utiliser les librairies.*)

Lemma p_inj: forall a b c:nat, a+b = a+c -> b=c.
Proof.
induction a.
simpl.
intros.
assumption.
intros.
rewrite plus_Sn_m in H.
rewrite plus_Sn_m in H.
apply eq_add_S in H.
apply IHa.
assumption.
Qed.

Lemma dist_gauche: forall a b c:nat, c*(a+b)=(c*a+c*b).
Proof.
induction a.
simpl.
intros.
rewrite <- mult_n_O.
simpl.
reflexivity.
intros.
simpl.
rewrite <-mult_n_Sm.
rewrite p_comm.
rewrite <-mult_n_Sm.
assert ( c * a + c =c + c*a).
apply p_comm.
rewrite H.
rewrite <- p_asso.
apply f_equal with (f:= plus c).
apply IHa.
Qed.

Lemma dist_droite: forall a b c:nat, (a+b)*c =(a*c+b*c).
Proof.
induction a.
simpl.
reflexivity.
simpl.
intros.
rewrite <- p_asso.
apply f_equal with (f:= plus c).
apply IHa.
Qed.

Lemma m_asso: forall a b c:nat, a*(b*c)= (a*b)*c.
Proof.
induction a.
simpl.
intros.
reflexivity.
simpl.
intros.
rewrite dist_droite.
rewrite IHa.
reflexivity.
Qed.

Lemma m_comm: forall a b:nat, a*b = b*a.
induction a.
simpl.
intro.
rewrite <- mult_n_O.
reflexivity.
simpl.
intros.
rewrite <- mult_n_Sm.
rewrite IHa.
apply p_comm.
Qed.

Lemma integrite: forall a b:nat, a<>0 -> b<>0 -> a*b <> 0.
Proof.
intros.
destruct a.
simpl.
assumption.
destruct b.
assert (0=0).
reflexivity.
contradiction.
simpl.
discriminate.
Qed.

Lemma m_inj: forall p q r:nat,r<>0 -> p*r = q*r -> p = q.
Proof.
induction p.
intros.
destruct q.
reflexivity.
assert (0*r=0).
compute.
reflexivity.
rewrite H1 in H0.
destruct  integrite with (a:= S q) (b:= r).
discriminate.
assumption.
apply eq_sym.
assumption.
intro.
intro.
simpl.
destruct q.
simpl.
destruct r.
assert (0=0).
reflexivity.
intro.
contradiction.
rewrite plus_Sn_m.
assert (S (r + p * S r) <> 0 ).
discriminate.
intros.
contradiction.
simpl.
intros.
apply eq_S.
apply IHp with (r:=r).
assumption.
apply p_inj with (a:=r).
assumption.
Qed.

(*COQ possède déjà < et <= mais elles ne sont pas pratiques pour ce que 
je veux faire, j'ai introduit les miennes*)
Definition inf_large (a b:nat):Prop:= exists p:nat, a+p = b.
Definition inf_strict (a b:nat):Prop:= exists p:nat, a+ (S p) = b.

Lemma lien_strict_large: forall x y:nat, inf_large x y <-> inf_strict x y \/ x=y.
Proof.
intros.
unfold inf_large.
unfold inf_strict.
split.
intros.
destruct H.
destruct x0.
right.
rewrite <- plus_n_O in H.
assumption.
left.
exists  x0.
assumption.
intros.
destruct H.
destruct H.
exists (S x0).
assumption.
rewrite H.
exists 0.
rewrite plus_n_O.
reflexivity.
Qed.

Lemma pas_deux_inegalites:forall a b:nat, ~(inf_large a b /\ inf_strict b a).
Proof.
intros.
unfold inf_large.
unfold inf_strict.
intro.
destruct H.
destruct H.
destruct H0.
rewrite <- H0 in H.
rewrite <- p_asso in H.
 cut((S x0 + x) = 0).
rewrite plus_Sn_m.
discriminate.
apply p_inj with (a:=b) (b:= (S x0 + x)) (c:=0).
rewrite <- plus_n_O.
assumption.
Qed.

Lemma ineg_large_disjunction: forall a b:nat,  inf_large a b \/ inf_large b a.
Proof.
induction a.
intros.
unfold inf_large.
left.
exists b.
rewrite plus_O_n.
reflexivity.
intro.
destruct IHa with (b:=b).
unfold inf_large.
apply lien_strict_large in H.
destruct H.
unfold inf_strict in H.
left.
destruct H.
exists x.
rewrite plus_Sn_m.
rewrite plus_n_Sm.
assumption.
right.
exists 1.
rewrite H.
rewrite p_comm.
reflexivity.
unfold inf_large.
apply lien_strict_large in H.
destruct H.
unfold inf_strict in H.
right.
destruct H.
exists (S (S x)).
rewrite <- plus_n_Sm.
apply eq_S.
assumption.
right.
exists 1.
rewrite p_comm.
rewrite H.
reflexivity.
Qed.

Lemma ineg_large_strict_disjunction: 
forall a b:nat,  inf_large a b \/ inf_strict b a.
Proof.
intros.
destruct ineg_large_disjunction with (a:=a) (b:=b).
left.
assumption.
apply lien_strict_large in H.
destruct H.
right.
assumption.
left.
unfold inf_large.
exists 0.
apply eq_sym.
rewrite <- plus_n_O.
assumption.
Qed.


Theorem induction_large: forall P:nat -> Prop, 
(forall q:nat, (forall r:nat, inf_strict r q -> P r)-> P q)-> forall n:nat, P n.
Proof.
intros.
assert (forall u v w:nat,u+w= S v -> u = S v \/ (inf_large u v)) as LEMMA1.
intros.
destruct w.
left.
rewrite <- plus_n_O in H0.
assumption.
right.
unfold inf_large.
exists w.
rewrite <- plus_n_Sm in H0.
apply eq_add_S.
assumption.
assert (forall m:nat, forall k:nat, inf_large k m -> P k) as LEMMA2.
induction m.
unfold inf_large.
intros.
destruct H0.
destruct k.
apply H.
intro.
intro.
unfold inf_strict in H1.
destruct H1.
rewrite <- plus_n_Sm in H1.
assert (S (r + x0) <> 0).
discriminate.
contradiction.
assert (S k +x <> 0).
rewrite plus_Sn_m.
discriminate.
contradiction.
unfold inf_large.
intros.
destruct H0.
apply LEMMA1 in H0.
destruct H0.
rewrite H0.
apply H.
intros.
apply IHm.
destruct H1.
unfold inf_large.
exists x0.
apply eq_add_S.
rewrite plus_n_Sm.
assumption.
apply IHm.
assumption.
apply LEMMA2 with (m:=n) (k:=n).
unfold inf_large.
exists 0.
apply eq_sym.
apply plus_n_O.
Qed.

Lemma pair_ou_impair: forall n:nat, exists p:nat, n=2*p \/ n = 1+2*p.
Proof.
induction n.
exists 0.
left.
compute.
reflexivity.
destruct IHn.
destruct H.
exists x.
right.
rewrite H.
simpl.
reflexivity.
exists (S x).
left.
rewrite H.
simpl.
rewrite plus_n_Sm.
reflexivity.
Qed.

Ltac cr:= compute; reflexivity.

Lemma mais_pas_les_deux: forall p:nat, forall q:nat, 2*p <> 1+2*q.
Proof.
induction p.
intros.
discriminate.
intros.
intro.
destruct q.
assert (1+2*0=1).
cr.
rewrite H0 in H.
unfold mult in H.
rewrite plus_Sn_m in H.
simpl in H.
assert (p+ (S p + 0)=0).
apply eq_add_S.
assumption.
rewrite plus_Sn_m in H1.
rewrite <- plus_n_Sm in H1.
assert (S (p + (p + 0)) <> 0).
discriminate.
contradiction.
intros.
rewrite <-mult_n_Sm in H.
rewrite <-mult_n_Sm in H.
rewrite p_comm in H.
assert (1 + (2 * q + 2)=2+(1+2*q)).
rewrite p_comm with (a:=2) (b:= (1+2*q)).
apply p_asso.
rewrite H0 in H.
unfold plus in H.
apply eq_add_S in H.
apply eq_add_S in H.
destruct IHp with (q:=q).
assumption.
Qed.

Lemma carre_impair: forall n:nat, (1+2*n)* (1+2*n)= 1+ 2* (2*n + 2* (n*n)).
Proof.
simpl.
intro.
apply eq_S.
rewrite p_asso.
rewrite <- p_asso.
rewrite <- p_asso.
rewrite <- p_asso.
rewrite <- p_asso.
rewrite <- p_asso.
apply f_equal with (f:= plus n).
rewrite <- p_asso.
apply f_equal with (f:= plus n).
simpl.
rewrite <- mult_n_Sm.
rewrite <- plus_n_O.
rewrite <- plus_n_O.
rewrite <- plus_n_O.
rewrite dist_gauche.
rewrite dist_droite.
rewrite <- p_asso.
apply f_equal with (f:= plus (n * n + n * n)).
rewrite p_comm.
reflexivity.
Qed.

Lemma carre_pair: forall n:nat, (2*n)*(2*n)= 2* (2*n*n).
(*remarque a posteriori: ce nn'était pas nécessaire de prouver ça*)
Proof.
intros.
rewrite <- m_asso.
apply f_equal with (f:= mult 2).
rewrite m_comm.
reflexivity.
Qed.

(*le résultat qu'on veut prouver est là*)

Theorem sqrt2_irrationnel: forall p:nat, p<>0 -> (forall q:nat,p*p <> 2*q*q).
Proof.
intro.
apply induction_large with (P:=fun (a:nat) => a<>0 -> (forall q:nat,a*a <> 2*q*q)).
intros.
assert (q*q<>0).
destruct q.
simpl.
assumption.
simpl.
discriminate.
intro.
assert (q0 <> 0).
intro.
rewrite H3 in H2.
rewrite H2 in H1.
apply H1.
cr.
destruct pair_ou_impair with (n:=q).
destruct H4.
rewrite H4 in H2.
rewrite <- m_asso in H2.
rewrite <- m_asso in H2.
rewrite m_comm in H2.
assert (2*(q0 * q0)=(q0 * q0)* 2).
apply m_comm.
rewrite H5 in H2.
apply m_inj in H2.
rewrite m_comm in H2.
apply eq_sym in H2.
assert (q0 * q0 <> 2 * x * x).
apply H.
destruct ineg_large_strict_disjunction with (a:=q) (b:=q0).
unfold inf_large in H6.
destruct H6.
rewrite H4 in H6.
rewrite <- H6 in H2.
rewrite dist_gauche in H2.
rewrite dist_droite in H2.
assert (2*x*(2*x)=2*x*x + 2*x*x).
simpl.
rewrite dist_gauche.
rewrite <- plus_n_O.
reflexivity.
rewrite H7 in H2.
rewrite <- p_asso in H2.
rewrite <- p_asso in H2.
assert (2 * x * x + (2 * x * x + (x0 * (2 * x) + (2 * x + x0) * x0)) 
= 2 * x * x+0).
rewrite <- plus_n_O.
assumption.
apply p_inj in H8.
assert (2 * x * x + (x0 * (2 * x) + (2 * x + x0) * x0) <> 0).
destruct x.
assert (q=0).
rewrite H4.
cr.
contradiction.
simpl.
discriminate.
contradiction.
assumption.
assumption.
contradiction.
discriminate.
rewrite H4 in H2.
rewrite <- m_asso in H2.
rewrite carre_impair in H2.
apply eq_sym in H2.
apply mais_pas_les_deux with (p:=q0 * q0) (q:= 2 * x + 2 * (x * x)).
assumption.
Qed.

christophe c · September 2020

De mon téléphone @fdp. Tout ceci a été expliqué 1001 fois en détails sur le forum et pas seulement par moi.

Si "non" te gêne oublie la.

Idem avec le mot absurde.

Le RPA est l'axiome qui te dit que

SI (A=>B) implique A

ALORS A.

christophe c · September 2020

Je recommande aux uns ou aux autres d'arrêter de vouloir mettre un clivage entre soit disant logiciens "enculeurs de mouches" et matheux "sociables et buvant du rouge sur les marchés".

Vouloir s'enfermer dans le fait que la valeur d'une phrase soit dans {vrai; faux} relève d'esprits obtus de même profil que ceux qui disaient que le bon sens implique la platitude de la Terre parce que tout bonnement sinon ceux qui ont la tête à l'envers tomberaient dans le vide.

La valeur d'une phrase que vous pouvez voir comme un ouvert d'un espace topologique les points étant les contextes et ceux lui appartenant ceux où elle est vraie si vous voulez, n'a pas de raison d'être l'intérieur de son adhérence sauf si un axiome l'impose. Ça ne va pas plus loin. Et c'est des maths assumées. Le "bon sens" non déductif du beauf local renvoie aux axiomes et non aux raisonnements. Restez scientifiques.

Foys · September 2020

La logique n'est jamais qu'une prise de distance vis-à-vis du langage mathématique qui est alors étudié comme un objet mathématique (vous avez des ensembles de suites de symboles appelés "formules", d'autres ensembles de suites de symboles appelés démonstrations, des sous-ensembles remarquables desdits ensembles -l'ensemble des démonstrations intuitionnistes étant strictement contenu dans celui des démonstrations dites classiques; et enfin une abondante accumulation de résultats de recherche qui date de plus d'un siècle -donc les jérémiades à base de "c'est une lubie récente", et "de mon temps", sont à éviter).
Sa situation est la même que celle de la grammaire française vis-à-vis du français: dans les petites classes, le maître décrit (ou en tout cas décrivait- quand j'y étais) les éléments de la langue devant ses élèves sans traumatisme psychologique.

A aucun moment dans les interventions de ce fil la preuve de l'irrationnalité de $\sqrt 2$ qui a été présentée (et qui est la plus répandue) n'a été dénigrée ou sa validité, remise en cause. (Vous croyez que si? indiquez un lien avec le message incriminé et le passage en, question).
Ce qui a été critiqué est la qualification incorrecte d'un élément de cette preuve comme étant un "raisonnement par l'absurde". Cette erreur est digne de "15 est un nombre premier", et c'est cela qui a attiré des réactions.

Dom · September 2020

Foys,

Là tu ajoutes de l’eau au moulin qui tourne en disant « c’est un truc des spécialistes qui dérangent les diptères » (Christophe, là quand même tu seras d’accord... non ?).
Je ne vais pas lire ça. J’ai posté des choses longues...mais là...

Moi, je veux faire voir à tout le monde (sans exception) que l’on est d’accord sur un point (je préciserai en faisant une synthèse très simple et courte, je le promets !) mais que beaucoup gardent des choses dans leurs têtes et ne les écrivent pas.

Quand les pros disent « ce n’est pas un RPA » ils parlent de la copie rendue.
À un oral ils demanderaient « attendez, comment ça vous faites un RPA ? vous avez démarré avec $\sqrt{2}$ est rationnel, expliquez moi un peu là... ?!?!!! ».
La majorité des candidats dira « heu...oui ! Je suppose que ce n’est pas vrai donc ça revient à $\sqrt{2}$ est rationnel ». ****

Et là, les pros sont obligés d’acquiescer** qu’il s’agit bien dans la tête du candidat d’un RPA.
Ils ajouteront ensuite : on pouvait s’en passer grandement, voyons !

**J’attends qu’un pro me dise que j’ai tort...

**** C’est exactement ce que disent Fin de partie et Chaurien. En effet, Fin de partie fait bien un RPA dans sa tête. Il dit bien et je le crois que pour lui c’est une étape tellement peu importante qu’elle est implicite.
Et je suis persuadé que tous les documents incriminés sont rédigés par des auteurs qui font la même chose.

Chaurien · September 2020

J'ai l'impression d'avoir déjà dit tout ce que j'avais à dire, et ce débat me fatigue. J'ai parcouru le texte d'Alain Prouté communiqué par Dom, très intéressant, mais je n'ai pas tout compris. Dans mon apprentissage classique de la logique, non(non p), c'est p, et puis voilà, je ne vois pas pourquoi il faudrait changer ça.
En page 5, Il propose un choix :
« $\bullet$ abandonner le tiers exclu et faire des mathématiques constructives.
$\bullet$ abandonner les ensembles infinis et faire des mathématiques finitistes
$\bullet$ abandonner les exigences constructivistes et faire des mathématiques classiques. »
Vous aurez certainement deviné mon choix, je pense. Je ne trouve pas, mais alors pas le moindre intérêt, à borner l'étude mathématique selon les deux premières exigences, qui me semblent complètement absurdes, c'est le cas de le dire. Chacun peut certes délimiter l'objet de son étude personnelle selon tel ou tel critère, en raison de ses préférences, mais en faire un principe universel de délimitation me semble tout à fait ridicule.
Bonne journée.
Fr. Ch.

Dom · September 2020

Merci Chaurien pour cette réponse.
Peut-être qu’en écrivant en début de copie ce que tu prends soin de nous dire serait très salvateur pour tout le monde.
A savoir « non(non(P)), c’est P ». Je ne dis pas de « changer ça ». Je dis que c’est une étape de ton raisonnement.
C’est seulement cela que je commente.

df · September 2020

La démonstration du théorème de Cantor (L’ensemble des parties d’un ensemble est plus grand que cet ensemble) est un bel exemple de démonstration par l’absurde (enfin je crois que s’en est une !)
La démonstration commence par: supposons qu’il existe une bijection d’un ensemble $E$ infini sur l’ensemble de ses parties.
Appelons $S$, l’ensemble des éléments de $E$ appariés à une partie de $E$ qui ne les contient pas.
La structure logique de la preuve est la suivante:

$\textbf{Si}$ $P=${Il existe une bijection entre E et l’ensemble de ses parties} $\textbf{alors}$ $Q=${Il existe une partie S de E ne pouvant être appariée à aucun élément de E}.
$\textbf{Si}$ $Q$ $\textbf{alors}$ NON-$P$; $\textbf{donc}$ NON-$P$.
...

SERGE_S · September 2020

Tout ce débat Byzantin sur le sexe des anges n'a aucune raison d'exister. Les mathématiques traditionnelles i.e. celles qui se pratiquent du CM jusqu'a M2 utilisent la logique classique pour les raisonnements. Donc ce débat comme le dit Chaurien n'a pas lieu d'être. Pour la logique classique non (non A) = A. Les démonstrations qui nient soit A soit (non A) pour aboutir à une contradiction sont surprise surprise des démonstrations par l'absurde et parfaitement légitimes.

Pour ceux qui pratiquent la logique intuitionniste où non (non A) n'est pas égale à A une distinction doit exister entre les deux méthodes de démonstration. Mais ce problème est en dehors de l'expérience de 90% des mathématiciens professionels et 100% des étudiants.

Dom · September 2020

Serge,

Justement, plus on est à un niveau bas, je dis qu’il faut rédiger cette étape (non(non(P)), c’est P.
Ça prend une ligne.
Mon point de vue n’est pas une discussion sur le sexe des anges.

Dom · September 2020

Serge,

Je n’ai pas compris cette phrase : « Pour la logique classique non (non A) = A. Les démonstrations qui nient soit A soit (non A) pour aboutir à une contradiction sont surprise surprise des démonstrations par l'absurde et parfaitement légitimes. »

Foys · September 2020

Revenons quelques jours en arrière.
Un usager, amo160, demande dans ce message de l'aide pour une preuve très répandue d'un résultat (l'irrationnalité de racine de 2).
Il met un extrait d'un livre qui commence par "supposons par l'absurde que sqrt 2 € Q". Bon cette qualification (non la preuve en elle-même) est fautive mais on commence à avoir l'habitude.

Ensuite, Fin de partie enfonce le clou avec ce message, insistant sur l'affirmation fautive en la soulignant.

Fin de partie. a écrit:

Amo160:

Ne perds pas de vue que c'est une preuve par l'absurde.

Là je suis obligé de poster.

****************************

Allégorie...

<<
-Alice: dans mon livre de recettes, j'ai du mal à comprendre cette phrase:
"après que vous ayez salé l'eau de cuisson, vous versez 100 grammes de pâtes"
-Endgame: qu'est ce qui ne va pas? "après que" est suivi du subjonctif
-un prêtre byzantin: non: "après que" est suivi de l'indicatif et la bonne tournure de phrase est "après que vous avez salé l'eau, vous versez 100 grammes de pâtes"
-Endgame: mais non c'est la bonne recette?
-Dzeta: à chaque fois que je demande autour de moi, les gens me confirment "qu'après qu'ils aient mis le sel, ils mettent les pâtes" et puis au diable ces histoires de grammaire.
-Charles M. : et cela continue. A chaque fois qu'on aborde ce sujet, un grammairien dans sa tour d'ivoire vient maltraiter les insectes. J'ai toujours mis le sel dans l'eau des pâtes avant les pâtes.
....
etc
>>

Dom · September 2020

Message aux pros en particulier (Foys, Christophe, ...)
Dans le papier que je cite, ici http://www.les-mathematiques.net/phorum/read.php?3,2089942,2091508#msg-2091508 je comprends que

-réduction de l’absurde, c’est juste démontrer la négation de quelque chose.
Pour démontrer non(P), je démontre (P=>tout) ce qui conduit, voire qui est la négation de P.

-détour par l’absurde, c’est faire un RPA
Pour démontrer P, je démontre (nonP=>tout) et j’en déduis P avec l’axiome RPA.

a) Est-on d’accord ?
b) avouez-vous que « preuve par l’absurde » ou « démonstration par l’absurde » est on ne peut plus ambigu à cause de ce terme « absurde » ?

Bien entendu, s’il faut jeter cette source à la poubelle, dites-le clairement.

side · September 2020

supp

SERGE_S · September 2020

@ Dom :

Démontrer la proposition A par l'absurde.
Hyp : supposons non A
Raisonnement mathématique conduit à une absurdité mathématique
Conclusion : non A est fausse donc A est vraie.

Démontrer la proposition non A par l'absurde
Hyp : supposons non(non A) c'est à dire suppons A (on est en logique classique)
Raisonnement mathématique conduit à une absurdité mathématique
Conclusion : A est fausse donc non A est vraie.

Le raisonnement par absurde dans les deux cas ci-dessus part en niant la chose (proposition mathématique) qu'on veut démontrer. Donc il n'y a pas lieu de distinguer entre le raisonnement par l'absurde de A ou de non A.

C'est seulement en logique intuitionniste que les deux approches ci-dessus sont différentes.

Fin de partie · September 2020

Foys:

Ta référence tombe à plat selon moi.
Ce n'est pas moi qui essaie de falsifier le sens d'une expression qui existait avant ma naissance et qui avait déjà le sens que je lui connais
Mon propos porte sur cette falsification du langage qu'un tas de gens acceptent sans broncher parce que les gens qui la pratiquent et la promeuvent ont une aura de gens sachant et qu'il faut toujours être du côté de ces gens-là si on ne veut pas passer pour un inculte et il ne faut pas froisser ces gens-là.

Ce n'est pas équivalent de dire, il n'y a pas un bout de tiers-exclus dans la démonstration classique de l'irrationalité de $\sqrt{2}$ et, ce n'est pas une démonstration par l'absurde. Pourtant j'ai bien l'impression que c'est ce que font un certain nombre de gens. L'escroquerie intellectuelle est poussée jusqu'à substituer une nouvelle définition pour appuyer leur thèse de ce qu'est une démonstration par l'absurde, après c'est facile de prétendre qu'il y a erreur sur la marchandise.

PS:
Curieusement pendant qu'on parlait de ça, il y avait ça:

J'y vois un lien entre les deux. B-)-

Dom · September 2020

Parfait :

C’est cela que je suggère d’écrire « Hyp : supposons non(non A) c'est à dire suppons A » mais Fin de partie et Chaurien y restent têtus.

Serge, on est d’accord.

df · September 2020

Side: je suis bien d’accord !
Personnellement, je n’ai jamais cru un seul instant que la logique était du « pinaillage » ou qu’elle consistait à faire subir les pires outrages à divers insectes !
C’est juste un domaine que je connais très mal !
Je signalais à @omega un article qui montrait des liens très étroits et passionnants entre la logique et l’algèbre.

cf: « Le problème de Tarski-algèbre et logique » par François Charles-RMS, numéro 3, Mai 2004.
...

Fin de partie · September 2020

Dom:

Notre désaccord sur le fond ne porte pas sur ce détail réellement.
Il y a des propositions dont il n'est pas immédiat quand on n'a pas quelques connaissances de formuler la négation, mais on parlait d'un cas précis où une proposition et sa négation sont facilement identifiables par quelqu'un qui a quelques peu de connaissances et elles apparaissent toutes les deux dans un raisonnement par l'absurde (dans le sens commun).
Si cela peut permettre de passer à autre chose je veux bien admettre que la phrase, supposons que $\sqrt{2}$ n'est pas irrationnel est préférable à, supposons que $\sqrt{2}$ est rationnel.
(cela suppose de prétendre vouloir démontrer donc que $\sqrt{2}$ est irrationnel)

Démontrer que racine de 2 n'est pas rationnel

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 3