Problèmes de logique

crikacrika · October 2017

Bonjour à tous,

J'ai commencé à voir le thème des démonstrations la semaine dernière et j'ai deux problèmes de preuves dont je ne semble pas trouver comment les faire.

1) Prouver par contraposée que si le produit de deux entiers positifs a et b est égal à n alors a^2 <= n ou b^2 <= n.
2) Prouver par contradiction que si a,b et c sont des nombres réels avec a différent de 0 alors l'équation ax+b = c admet une solution unique.

Je remercie d'avance ceux qui peuvent m'aider à résoudre ces problèmes(ou à me donner des pistes de solution).

Dom · October 2017

Bonjour,

Pour 1) je propose d'écrire la propriété avec des quantificateurs (à quel niveau ces exercices doivent-ils être résolus ?).
Puis d'écrire la contraposée.
On essaiera ensuite de voir ce qu'il "faut" prouver.

crikacrika · October 2017

Salut,

Que voulez-vous dire par "niveau"? Mon niveau d'études? Je suis à l'université.

Quant au niveau de résolution de la preuve, il n'était pas vraiment specifié, l'exercice était écrit tel qu'écrit.

crikacrika · October 2017

Quant aux quantificateurs, si on dit que P(a,b) vaut "Le produit de a et b donne n", ça donne:

Pour tout a et pour tout b P(a,b)

Donc avec tout le reste, ça donnerait:

Pour tout a et pour tout b P(a,b) => a^2 =< n V b^2 =< n

Dom · October 2017

On corrige une coquille : (on reste sur ton idée d'utiliser P(.,.) même si ce n'est pas nécessaire)

Pour tout a, b positifs, P(a,b)=n => (a^2=<n ou b=<n).

Maintenant la contraposée (de l'implication).

Pour tout a,b positifs, ...

NB : pardon, j'ai un sacré bug, pas de dollars en vue (mais pourtant le compte en banque va assez bien en début de mois).

remark · October 2017

.

christophe c · October 2017

l'exercice était écrit tel qu'écrit.

L'exercice n'a pas de sens. Que veut dire "prouver par X"? Que la preuve doit contenir X? On peut toujours faire la preuve qu'on veut et rajouter l'ingrédient X en bout de preuve.

A mon avis, la seule chose qu'on peut mettre qui aurait un sens en adverbe de la consigne prouver serait "sans utiliser Truc", ce qui donne "prouver sans utiliser Truc". C'est une manière pédagogique de supprimer des axiomes autorisés, mais au moins ça fait sens pour le correcteur.

Conique · October 2017

Au lieu d'ergoter de façon nombriliste dans un langage incompréhensible pour l'apprenant, essayez de lui apporter de l'aide. Et vous dites en plus que l'exercice que lui donne son prof est très artificiel et mal posé ? C'est des gars comme vous qui détruisez l'élan chez les étudiants.

fluorhydrique · October 2017

Prouver par contraposée que ....

L'exercice n'a pas de sens. Que veut dire "prouver par X"?

Le raisonnement par contraposée ça existe

si on lui demande de faire son raisonnement ainsi il ne va pas le faire autrement

remark · October 2017

.

Félix · October 2017

Bonjour,

Prouver avec contrainte est-il si étrange, si la contrainte en question est l'objet du cours et donc l'exercice destiné à s'entrainer sur les concepts que celui-ci a introduits ?

remark · October 2017

.

Félix · October 2017

Merci pour cet argument, qui me convainc.

Amicalement

pldx1 · October 2017

Bonjour.

Affirmation: Si le produit de deux entiers positifs $a$ et $b$ est égal à n alors $a^2 \leq n$ ou $b^2 \leq n$.
Une preuve possible. La proposition $a\times b=n$ équivaut à $a^2\times b^2 =n^2$ (nombres positifs). Appelons cela $A$.
Appelons $B$ la proposition $a^2 \leq n\; ou \;b^2 \leq n$. Réduisons $nonB$ à l'absurde en supposant $A$. On aurait $a^2>n$ et $b^2>n$ et donc $a^2b^2>n^2$. Quod erat delendum.

Il rest à habiller cela de façon contrapositoire. Et c'est fini (trois lignes).

On peut aussi en rajouter une couche selon le modèle

pdir:= (ply)(a,b);
prec:= (ply)(non(b),non(a));
ceti_vrai:= (rul@xet)(ply(pdir,prec), ply(prec,pdir));

$$ceti\_vrai \mapsto 1 $$

On peut aussi noyer les survivants par des incantations quantificatoires. On peut même utiliser le bon ordre des entiers pour invoquer la plus petite exception au sens lexicographique et la réduire à l'absurde comme ci-dessus.

Bref, il reste le critère: un nombre $n$ est premier s'il n'est divisible par aucun nombre premier inférieur ou égal à $\sqrt n$.

Cordialement, Pierre.

NB. On remarque encore et à nouveau que certains intervenants ne peuvent pas s'empêcher de prétendre que les enseignants sont nuls à chier et posent des exercices "artificiels et assez mal posés", pour ne pas dire "insensés". Il est difficile de s'empêcher de se demander d'où leur vient une pareille propension.

christophe c · October 2017

@conique: http://www.les-mathematiques.net/phorum/read.php?16,1537078,1537416#msg-1537416

Une faute est une faute, point! Personne n'érgote, en tout cas, ni remark, ni moi. Il faut arrêter de crier son désespoir qu'on voudrait arriver à donner un sens à des choses qui n'en ont pas, les cris ne vont pas faire apparaitre un sens ou un effacement de l'erreur par magie. Personne ne critique l'enseignant, on dit juste que l'exercice est formulé de manière fautive, j'ai détaillé pourquoi.

Je vais donc me répéter autrement:

règle: quand on donne un exercice de maths, il doit être formellement sans ambiguité ni difficulté de le corriger. Si une consigne n'est pas telle que quelle que soit la proposition de solution de l'étudiant, il est possible en quelques secondes de lui attribuer ou pas les points, alors cette consigne sort des maths et s'en trouve invalide.

Application: la consigne <<prouver en utilisant X>> est fautive puisqu'elle demande un "supplément" inutile de présence dans le texte, qui peut toujours être ajouté artificiellement. Certains objecteurs de mauvaise foi à ça pourraient répondre que l'ajout artificiel ne sera pas considéré comme une bonne réponse et qu'il faut qu'il soit naturel, mais dans ce cas, on n'est plus en maths, on est en correction de devoir de français (ou de philo), puisqu'il est laissé à l'appréciation du correcteur une notion de naturel qui ne veut rien dire.

Les débats sur le pédagogisme n'ont rien à voir avec cette question, et il est incorrect de tenter d'allumer malhonnêtement (malhonnêteté intellectuelle, j'entends) des contre-feux pour cacher les fautes avec slogan sous-entendu du genre "je méritais les points mais j'ai été victime d'une correctrice reac"

Cyrano · October 2017

Oui enfin, ça c'est en théorie. En pratique, on est quand même TRES content de pouvoir poser des questions du type :

"Calculer $$\int_0^{+\infty} \frac{\ln(x)}{x^2+2x+2} \, dx$$ en utilisant le théorème des résidus et simplifier au maximum votre réponse."

Là il y a carrément deux trucs qui ne sont pas des maths mais qu'il est vraiment pratique de pouvoir mettre. Il suffit de discuter avant avec l'élève pour lui expliquer que ce sont des notions de "bon sens". (Je suis d'accord ce ne sont pas des maths, mais le concept même d'examen avec durée limitée etc ... va souvent à l'encontre du fondement mathématique.)

christophe c · October 2017

@Cyrano, mais comme tu dis en pratique, ici il est clair que le correcteur acceptera n'importe quelle solution et qu'il donne juste une indication. Ce n'est pas du tout, mais alors pas du tout la même chose.

Dans le premier post de crika, avec mise en gras des mots "contraposée" et "contradiction", on est dans une toute autre situation:

1) "prouver par contraposée" ne veut rien dire (il y a erreur bête et méchante de grammaire mathématique).
2) il ouvre un fil pour demander spécifiquement ce que veulent dire "prouver par contraposée" ou "par contradiction".

On se doit donc de lui répondre que ça ne veut rien dire, point barre.

Alors que dans ton exemple, on sait très bien que ça veut dire "calculer X. Indication: on pourra** se servir de Y" (mais si quelqu'un trouvait, par miracle, une façon bien plus élégante de procéder, il est très clair que cette consigne n'ordonne pas au correcteur de retirer des points).

** la tournure étant une espèce, d'ailleurs, de clin d'oeil complice pour signaler aux étudiants que bien ambitieux serait celui qui essaierait de se passer de Y

Cyrano · October 2017

Ben je t'avoue que moi j'ai tendance à imposer la méthode dans ce contexte.
Si le contexte est un cours d'analyse complexe, je me fous de savoir si l'étudiant est un génie de la primitivation (tant mieux pour lui cela dit), je veux voir sa capacité à appliquer les résidus donc j'impose la méthode. Mais alors, comme c'est un ordre non mathématique, j'explique oralement ce que je veux dire par là.
En général ça ne pose vraiment aucun problèmes à personne ... (Et comme tu dis, de toute façon, personne n'a jamais l'ambition de faire autrement.) Il n'empêche que dans le cadre d'un examen (et uniquement ce cadre) on peut vouloir IMPOSER une méthode juste pour vérifier que l'élève maîtrise cette méthode (et pas une autre).

Ca parait évidemment absurde pour un chercheur qui ne s'impose jamais rien si ce n'est de trouver une preuve. Mais pour un étudiant, ça me semble quand même parfois important.

Cela dit nous sommes d'accord qu'ici l'énoncé de l'auteur est mauvais.

Conique · October 2017

Bonjour,

@remark @christophe c J'ai lu avec intérêt vos interventions.

Je me suis un peu emporté hier soir, si vous voulez bien m'excuser. Je crois que je voyais juste un étudiant voulant progresser dans un problème se faire reprocher quelque chose dont il n'est pas responsable, dont il n'a pas la charge : l'énoncé, le contenu même de son problème. Il n'en est pas responsable parce qu'il débute, non pas parce qu'il est étudiant. La lecture critique des énoncés fait en effet partie intégrante de l'activité mathématique.

Je partage vos points de vue, à la fois sur les choses importantes à apporter à des étudiants dans le supérieur, à la fois sur le caractère bien fondé (ou non) d'une formulation de problème, ici malheureuse je le reconnais.

Concernant la critique de @remark, qui concerne la quantification, et la discussion de @christophe c sur la fine limite entre suggestion et contrainte dans un énoncé, je propose le point de vue suivant. La contraposée d'une implication n'est-elle tout simplement une écriture logiquement équivalente à cette implication ? Si oui, alors la phrase, (qui n'est pas correcte, je rejoins @christophe c là-dessus), "prouver par contraposée" (par contraposition aurait peut-être été un peux moins faux), ne veut-elle pas dire, mais maladroitement : "faire la démonstration en identifiant une implication puis en montrant son implication contraposée" ? Si oui encore, alors en effet, il y a un réel besoin d'identification d'une implication à faire par l'étudiant, afin qu'il puisse écrire correctement sa contraposée. Or, elle n'est pas du tout bien mise en valeur dans le présent énoncé, ce qui rend difficile car flou le chemin pour résoudre l'exercice. Ajoutons à cela une quantification bancale, utilisons la règle de @christophe c sur la nécessaire limpidité de correction d'un énoncé, et l'on voit qu'on est en face d'un problème mal rédigé, oui. Il y a donc une faute de l'enseignant.

Pour la pallier et aider l'étudiant, @remark a proposé une meilleure formulation et a jugé l'exercice de peu d'intérêt, et @christophe c a d'office détruit l'énoncé, infondé logiquement.
Cependant, de mon point de vue, l'aspect psychologique est à ne pas négliger. Lorsque je cherche à plancher sur un énoncé, j'ai besoin d'avoir une certaine, disons, confiance en lui, le trouver intéressant, élégant, difficile, riche, différent-des-autres, ... ce que l'on voudra qui le rende motivant. La négation de l'intérêt d'un énoncé ou d'un professeur n'est jamais une bonne solution, j'en suis presque convaincu. Cela ne peut amener l'élève qu'à laisser de côté ce qu'il a devant lui. Cela n'est pas interdit, mais alors il faut immédiatement le recadrer avec un meilleur énoncé, quelque chose qui vienne remplacer ce qu'on vient de nier. Donc : oui, une faute est une faute. Cela n'empêche qu'il faut ensuite apporter le terreau de la motivation par un moyen ou par un autre.

Enfin, sur le caractère naturel d'une preuve, certes, les preuves directes sont presque toujours plus belles, mieux construites. Néanmoins, ce que, @remark, tu qualifies de naturel, est en fait éminemment culturel. Il faut toute une éducation mathématique à un esprit pour bien comprendre ce que ce mot veut dire. Il faut notamment des preuves biscornues, y compris des preuves longues, y compris des preuves chiantes, il faut de l'exercice dans tous les sens... Car sans ces dernières, comment la puissance de celles qui ne le sont pas, celles qui aideront l'étudiant à se forger une idée de ce qu'est une preuve naturelle, pourra apparaître ?

Là, c'est moi qui commence à ergoter, à parler pour ne rien dire, alors je m'arrête ici. Bonne journée.

remark · October 2017

.

pldx1 · October 2017

D'après wp:fr, l'origine de l'expression "contraposée" en français est une traduction (1862) de la Logique d'Emmanuel Kant
http://gallica.bnf.fr/ark:/12148/bpt6k5400803z/f195.item.r=contraposée. Si non e vero, e ben trovato !

Et donc l'expression exacte serait: raisonnement per judicia contraposita. Se contenter de dire "raisonnement par contraposition" semble moins snob, malgré tout.

Foys · October 2017

Le raisonnement par contraposée consiste à partir de $A\to B$, à déduire $\neg B \to \neg A$.

pldx1 · October 2017

Bonjour,

La question posée était de prouver par contraposition que "si le produit de deux entiers positifs a et b est égal à n alors a^2 <= n ou b^2 <= n", énoncé que l'on peut modéliser par "si A, alors B". Bien entendu, il n'est pas question de partir de "si A, alors B".

Nous partons de $non B$. Supposons donc que : $a^2 > n \;et\; b^2 > n$. Par positivité, on en déduit: $a^2\times b^2 > n^2$. Par croissance du carré, ceci donne $ab>n$. Prouvant $non A$. Nous avons donc: $non B \implies non A$. Comme cette implication est la contraposée de l'implication originelle, celle-ci est prouvée à son tour.

"Tant qu'à illustrer un schéma de preuve, il serait mieux de le faire sur un exemple où le schéma en question est naturel". Je ne vois rien de surnaturel dans les trois lignes qui précèdent. Quant à préférer $a\leq b \;ou\;b\leq a$ donc $a\times a\leq a\times b \;ou\;b\times b\leq b\times a$... cela demande deux multiplications au lieu d'une (sans parler de penser à remplacer $n$ par sa valeur...).

Cordialement, Pierre.

Foys · October 2017

Je n'ai pas précisé qui étaient $A$ et $B$ dans ma phrase qui était générale.
Les énoncés $(A\to

\to (\neg B \to \neg A)$ et $(\neg B \to \neg A)\to (A\to

$ ne sont pas les mêmes, en particulier seul le premier est valide en logique intuitionniste, l'autre non (il entraîne, avec les règles de manipulation habituelles de l'implication, le tiers exclus ). C'est bien ce premier type d'énoncé qui est mis à contribution lorsqu'on dit raisonner par contraposée.
La formulation de l'exercice est donc particulièrement maladroite.

remark · October 2017

.

pldx1 · October 2017

@Foys: Qu'est ce que crikacrika peut bien avoir à cirer de la logique intuitionniste pour résoudre son exercice ?

Autrement dit, quelles sont tes recommandations, pour crikacrika, quant aux valeurs des expressions
$non\left( a^2\leq n \;ou\; b^2\leq n\right)$ et $non\left( a^2 >n \;et\; b^2> n\right)$ ?

remark · October 2017

.

pldx1 · October 2017

Bonjour remark.

En fait, oui et non. Si le cours à illustrer est le crible d'Eratosthène, il n'y a pas une preuve "plus naturelle" qu'une autre et, en effet, cela relève de la question de goût. Si le cours à illustrer est "preuve par contraposition", "preuve par contradiction", cela relève de la "figure imposée" dans une épreuve de gymnastique: un Kovacs, ce n'est pas un salto avant.

Cordialement, Pierre.

Dom · October 2017

Le côté artificiel est certainement voulu : on fait travailler des notions de logiques, du vocabulaire, afin de le faire rentrer dans la tête. Le fait d'interdire un sens direct (disons dans le langage courant "un sens normal" pour énerver tout le monde) fait aussi parti d'un exercice d'abstraction. Je m'explique : on sait faire d'une manière et on s'intéresse à une autre, jugée saugrenue.

J'ai compris la remarque de @conique comme un "ras la casquette" de l'intervention de @cc (je parle du texte qu'il livre ici et non de lui !). C'était aussi envers @remark, mais comme cela a été dit, il propose au moins de participer à une aide et ne s'arrête pas à "c'est pourri".
Cela dit la recherche d'un énoncé formellement non ambiguë fait aussi parti de la pratique des Mathématiques.
Mais à ceci j'ajouterais "chaque chose en son temps" selon qui pose la question.

remark · October 2017

.

Dom · October 2017

2) (il faut vite réagir au mot "équation" qui n'est pas mathématique et surtout dire quelle est l'inconnue* dans $ax+b=c$ sinon l'exercice est ...)

Si $(a,b,c) \in \mathbb R^3$ et $a\neq 0$ Alors il existe un unique $x$ réel tel que $ax+b=c$.

Remarque : c'est la négation de "il existe un unique" qui pose des légers problèmes.
Mais là encore, l'exercice est fait pour ça, de mon point de vue.

[small]*sur ce point, c'est tout de même important, on peut critiquer sans faire de mauvais esprit[/small]

remark · October 2017

.

Dom · October 2017

Comme tu le dis, c'est moche, mais c'est le jeu ma pauvre Lucette.

On va démontrer :
Si (a,b,c) réels et a non nul et si NON(il existe un seul x tel que ax+b=c) alors $une\quad contradiction$.

Soient a un réel non nul et b et c deux réels et {1) pour tout x, ax+b $\neq$ c ou 2) il existe deux nombres distincts m et n tels que am+b=c et an+b=c}.

Dans le cas 1), on pose x=(c-b)/a et alors c'est contradictoire avec l'hypothèse.
Dans le cas 2), on déduit que : a(m-n)=0 alors contradiction avec les hypothèses.

C'est le point 1) qui est moche, disons, saugrenu.
On pourrait balancer : toute équation du premier degré possède une solution...bon c'est moche aussi...

[small]Pardon pour le manque de LateX, je modifierai plus tard (certains soirs je perds mes dollars, et l'astuce copier coller déconne - j'ai pu l'utiliser deux fois -, bref, c'est le moment de dépenser les euros...)[/small]

Foys · October 2017

pldx1 a écrit:

@Foys: Qu'est ce que crikacrika peut bien avoir à cirer de la logique intuitionniste pour résoudre son exercice ?

-Il faudrait que tu te calmes.
-Es-tu crikacrika? Si oui il me semble que les pseudos multiples ne sont pas les bienvenus sur le forum. Sinon je pense qu'il peut se plaindre lui-même. De plus mes remarques n'étaient pas adressées qu'à lui.

Pour ta deuxième question, il est possible de traiter l'exo via $non(a^2> n \wedge b^2 >n)$.

Foys · October 2017

On trouvera ci-dessous une solution de l'exercice 1 en Coq (qui complie chez moi avec la version 8.4)
Les longueurs viennent surtout de ce que la liste des résultats exploitables en arithmétique disponibles dans Coq est
très dépouillée, il faut tout faire soi-même et j'ai voulu épargner à chacun la recherche et l'installation de librairies aussi en ai-je inclus une (qui ne contient absolument aucun résultat original ou étrange).
C'est à mon avis un bon exercice que de faire ce genre de choses (au lieu de chercher à intuiter les bonnes règles de rédaction).
Au passage il se trouve que l'exo est faisable de manière intuitionniste. L'arithmétique de Heyting est moins handicapée qu'elle n'en a l'air au premier abord.
Bonne lecture!

Lemma contraposee: forall a b:Prop, (a->b) -> (~b -> ~a).
Proof.
intros.
intro.
apply H0.
apply H.
assumption.
Qed.

Section lemmes_arithmetiques.
Lemma lemme_a0: forall x:nat, 0 <= x.
Proof.
induction x.
apply le_n.
apply le_S.
assumption.
Qed.

Lemma lemme_a1: forall x y:nat, x<=y -> S x <= S y.
Proof.
intro.
apply le_ind.
apply le_n.
intros.
apply le_S.
assumption.
Qed.

Lemma lemme_a2:forall x y:nat,
x < y \/ y<= x.
Proof.
induction x.
induction y.
right.
apply le_n.
left.
unfold lt.
apply lemme_a1.
apply lemme_a0.
intro.
destruct IHx with (y:=y).
unfold lt in H.
destruct H.
right.
apply le_n.
left.
unfold lt.
apply lemme_a1.
assumption.
right.
apply le_S.
assumption.
Qed.

Lemma lemme_a3: forall x y z:nat, y <= z -> x<= y ->  x <= z.
Proof.
intro.
intro.
intro.
intro.
apply le_ind with (n0:=z) (n:=y).
intros.
assumption.
intros.
assert (x<= m).
apply H1.
assumption.
apply le_S.
assumption.
assumption.
Qed.

Lemma lemme_a4: forall a b:nat, a+b = b+a.
Proof.
induction a.
intro.
assert (0+b = b).
apply plus_O_n.
assert (b=b+0).
apply plus_n_O.
rewrite H.
assumption.
intro.
assert (S a+ b = S(a+b)).
apply plus_Sn_m.
assert (S(a+b)=S(b+a)).
assert (a+b=b+a).
apply IHa.
rewrite H0.
reflexivity.
rewrite H.
rewrite H0.
apply plus_n_Sm.
Qed.

Lemma lemme_a5: forall a b:nat, a*b=b*a.
Proof.
induction a.
intro.
assert (0*b=0).
simpl.
reflexivity.
assert (0=b*0).
apply mult_n_O.
rewrite H.
rewrite <-H0.
reflexivity.
intro.
simpl.
assert (b*a+b=b* S a).
apply mult_n_Sm.
rewrite <-H.
assert (a*b=b*a).
apply IHa.
rewrite H0.
apply lemme_a4.
Qed.


Lemma lemme_a6: forall x y a:nat,x<y -> a+x < a+y.
Proof.
intro.
intro.
induction a.
intro.
simpl.
assumption.
intro.
simpl.
unfold lt.
apply IHa in H.
unfold lt in H.
apply lemme_a1.
assumption.
Qed.

Lemma lemme_a7: forall a b:nat, (exists c:nat, a+c=b) <-> (a <= b).
Proof.
assert (forall a b c:nat,  a+c=b -> (a <= b)).
intro.
intro.
assert (forall x:nat, a<= a+x).
induction x.
assert (a=a+0).
apply plus_n_O.
rewrite <-H.
apply le_n.
assert (S(a+x)=a+S x).
apply plus_n_Sm.
rewrite <-H.
apply le_S.
assumption.
intros.
rewrite <-H0.
apply H.
assert (forall a b:nat, a<= b -> exists c : nat, a + c = b).
intro.
apply le_ind.
exists 0.
assert (a=a+0).
apply plus_n_O.
rewrite <-H0.
reflexivity.
intros.
destruct H1.
exists (S x).
rewrite <-H1.
assert (S(a+x)=a+S x).
apply plus_n_Sm.
rewrite H2.
reflexivity.
intros.
split.
intro.
destruct H1.
apply H with (c:=x).
assumption.
apply H0.
Qed. 

Lemma lemme_a8:forall a b:nat, (exists c:nat, a+S c=b) <-> (a < b).
Proof.
intro.
intro.
split.
unfold lt.
intros.
destruct H.
assert (S(a+x)=a+S x).
apply plus_n_Sm.
assert (S a + x= S (a+x)).
apply plus_Sn_m.
rewrite <-H1 in H0.
rewrite <-H0 in H.
apply lemme_a7.
exists x.
assumption.
unfold lt.
intro.
assert (exists d : nat, S a +  d = b).
apply lemme_a7.
assumption.
destruct H0.
assert (S a + x= S (a+x)).
apply plus_Sn_m.
assert (S(a+x)=a+S x).
apply plus_n_Sm.
exists x.
rewrite <-H2.
rewrite <-H1.
assumption.
Qed.

Lemma lemme_a9: forall a b c:nat, (a+b)+c = a+ (b+c).
Proof.
induction a.
intros.
assert (0+b=b).
apply plus_O_n.
rewrite H.
assert (0+(b+c)=b+c).
apply plus_O_n.
rewrite H0.
reflexivity.
intros.
assert (S a + b = S (a+b)).
apply plus_Sn_m.
rewrite H.
assert (S(a+b) + c = S ((a+b)+c)).
apply plus_Sn_m.
rewrite H0.
assert (S a + (b+c) = S(a+ ( b+c))).
apply plus_Sn_m.
rewrite H1.
assert (a+b+c = a+ (b+c)).
apply IHa.
rewrite H2.
reflexivity.
Qed.

Lemma lemme_a10: (forall a b c:nat, a*b+a*c = a*(b+c))
/\ (forall a b c:nat, b*a+c*a = (b+c)*a).
Proof.
assert (forall a b c:nat, b*a+c*a = (b+c)*a).
intro.
intro.
induction c.
assert (0*a=0).
simpl.
reflexivity.
rewrite H.
assert (b*a=b*a+0).
apply plus_n_O.
rewrite <-H0.
assert (b=b+0).
apply plus_n_O.
rewrite <-H1.
reflexivity.
simpl.
assert (S(b+c)=b+S c).
apply plus_n_Sm.
rewrite <- H.
simpl.
assert (a+c*a = c*a + a).
apply lemme_a4.
rewrite H0.
assert (b*a+ c*a+a = b*a + (c*a + a)).
apply lemme_a9.
rewrite <- H1.
assert (a+ (b+c)*a = (b+c)*a + a).
apply lemme_a4.
rewrite H2.
rewrite IHc.
reflexivity.
split.
intros.
assert (a*b = b*a).
apply lemme_a5.
assert (a*c = c*a).
apply lemme_a5.
assert (a*(b+c) = (b+c)*a).
apply lemme_a5.
rewrite H0.
rewrite H1.
rewrite H2.
apply H.
assumption.
Qed.

Lemma lemme_a11: forall a b c d:nat, a<c -> b<d -> a*b < c*d.
Proof.
intros.
assert (exists p:nat, a+S p = c).
apply lemme_a8.
assumption.
assert (exists q:nat, b+ S q = d).
apply lemme_a8.
assumption.
destruct H1.
destruct H2.
apply lemme_a8.
assert (c* (b+ S x0)= c*b+c*S x0).
apply eq_sym.
apply lemme_a10.
rewrite  H2 in H3.
assert(a*b + (S x)* b = c*b).
rewrite <-H1.
apply lemme_a10.
assert (a*(S x0)+ (S x* S x0) =c* S x0).
rewrite <-H1.
apply lemme_a10.
rewrite <-H5 in H3.
rewrite <- H4 in H3.
assert (S x * S x0 = S x0 + x * S x0).
simpl.
reflexivity.
assert (a * b + S x * b + (a * S x0 + S x * S x0)= a*b + (S x * b + (a * S x0 + S x * S x0))).
apply lemme_a9.
assert (a * S x0 + S x * S x0 = S x * S x0 + a * S x0).
apply lemme_a4.
(*rewrite H8 in H7.*)
assert (S x * b + (S x * S x0 + a * S x0) = S x * S x0 + a * S x0 + S x * b).
apply lemme_a4.
rewrite H7 in H3.
rewrite H8 in H3.
rewrite H9 in H3.
rewrite H6 in H3.
assert (S x0 + x * S x0= S (x0 + x * S x0)).
simpl.
reflexivity.
rewrite H10 in H3.
assert (S (x0 + x * S x0) + a * S x0=S (x0 + x * S x0 + a * S x0)).
simpl.
reflexivity.
rewrite H11 in H3.
assert (S (x0 + x * S x0 + a * S x0) + S x * b=S(x0 + x * S x0 + a * S x0 + S x * b)).
simpl.
reflexivity.
rewrite H12 in H3.
exists (x0 + x * S x0 + a * S x0 + S x * b).
apply eq_sym.
assumption.
Qed.

Lemma lemme_a12: forall  b c a:nat, (a*b)*c = a*(b*c).
Proof.
intro.
intro.
induction a.
simpl.
reflexivity.
simpl.
assert (b*c + (a*b)*c = (b+a*b)*c).
apply lemme_a10.
rewrite <- H.
rewrite IHa.
reflexivity.
Qed.

Lemma lemme_a13: forall x y:nat, x+S y <> x.
Proof.
induction x.
intros.
discriminate.
intros.
intro.
assert (S x + S y = S (x+ S y)).
apply plus_Sn_m.
rewrite H0 in H.
assert (x + S y = x).
apply eq_add_S.
assumption.
assert (x + S y <> x).
apply IHx.
contradiction.
Qed.

Lemma lemme_a14: forall x:nat, ~(x<x).
Proof.
intro.
intro.
assert (exists k:nat, x+S k=x).
apply lemme_a8.
assumption.
destruct H0.
apply lemme_a13 with (x:=x) (y:=x0).
assumption.
Qed.


End lemmes_arithmetiques.

Lemma lemme_pour_l_exo: forall (x y n:nat), ~(n<x /\ n<y) -> (x <= n \/ y<=n).
Proof.
intros.
assert (n<x \/ x <= n).
apply lemme_a2.
assert (n<y \/ y <= n).
apply lemme_a2.
destruct H0.
destruct H1.
destruct H.
split.
assumption.
assumption.
right.
assumption.
left.
assumption.
Qed.

Theorem exercice1: forall a b n:nat, a*b=n -> a*a <=n \/ b*b <=n.
Proof.
intros.
assert (a*b*a*b = a*a*(b*b)).
assert (a*b*a = a*(a*b)).
apply lemme_a5.
rewrite H0.
assert (a*(a*b)=a*a*b).
apply eq_sym.
apply lemme_a12.
rewrite H1.
apply lemme_a12.
apply lemme_pour_l_exo.
cut(~n*n <a*b*a*b).
apply contraposee.
intro.
rewrite H0.
apply lemme_a11.
apply H1.
apply H1.
assert (a*b*a*b=a*b*(a*b)).
apply lemme_a12.
rewrite H1.
rewrite H.
apply lemme_a14.
Qed.

Alesha · October 2017

"Prouver A par l'absurde", c'est montrer l'absurde (en supposant non A) pour en déduire A. On pourrait donc s'attendre à ce que "Prouver A par contraposée", c'est montrer la contraposée de A pour en déduire A, c'est-à-dire si A = $(B \Rightarrow C)$, prouver $(\neg C \Rightarrow \neg

$. Mais, Foys, tu sembles l'interpréter à l'opposé: ce serait prouver $(B \Rightarrow C)$ pour en déduire sa contraposée $(\neg C \Rightarrow \neg

$. Est-ce bien ce que tu veux dire?

Foys · October 2017

Alesha, oui et en fait c'est toujours dans ce sens que j'ai vu l'expression employée.
C'est vrai que l'exo est plus simple (et plus naturel aussi il faut quand même le reconnaître) si on décide de déduire la conclusion de l'exo de "$\neg(a^2\leq n\vee b^2 \leq n)\implies \neg (ab=n)$. Mais là on est dans le cadre d'un raisonnement par l'absurde en bonne et due forme.

oka · October 2017

je me rappelle dans un cours avoir dit à un prof que sa solution au tableau n'était pas un raisonnement par contraposée mais plutot un raisonnement par l'absurde ecrit maladroitement, alors que il l'avait introduite par "montrons par contraposée que..."

(il utilisait comme dit Foys un raisonnement de la forme $(\neg B \to \neg A)\to (A\to

$ )

ça a entrainé un debat de 20min et je ne crois pas avoir convaincu grand monde, surtout pas le prof. Des gens venaient meme me voir à la fin du cours en disant "il faudrait des cours de logique à la fac, certains ont du mal avec ça" (ironiquement bien sur)

Foys · October 2017

Le truc, c'est qu'avec les règles de déduction (naturelle par exemple) usuelles pour $\to$, si $\Gamma$ est l'ensemble de toutes les formules propositionnelles de la forme $(\neg B \to \neg A) \to (A \to

$ où $A,B$ sont des formules propositionnelles, (les parenthèses seront prioritaires à droite désormais donc je vais noter $(\neg B \to \neg A) \to A \to B$ et $\neg$ va être prioritaire sur $\to$) alors pour tout $X$, $\Gamma \vdash \neg \neg X \to X$. en effet:

Supposons $\neg \neg X$. Soit $P$ une formule propositionnelle quelconque.
Alors on a successivement:
$\Gamma,\neg \neg X, \neg \neg P \vdash \neg \neg X$ (axiome)
$\Gamma,\neg \neg X \vdash \neg \neg P \to \neg \neg X$.(introduction de $\to$)
$\Gamma,\neg \neg X \vdash (\neg \neg P \to \neg \neg X)\to \neg X \to \neg P$ (axiome)
$\Gamma,\neg \neg X\vdash \neg X \to \neg P$ (élimination de $\to$)
$\Gamma,\neg \neg X\vdash (\neg X \to \neg P) \to P \to X$ (axiome)
$\Gamma,\neg \neg X\vdash P \to X$ (élimination de $\to$).

et comme ceci est valable pour tout $P$, en remplaçant $P$ par une tautologie comme $X\to X$, on voit que
$\Gamma,\neg \neg X\vdash X$, donc (introduction de $\to$) que $\Gamma \vdash \neg \neg X\to X$.

Alors que $(A\to

\to \neg B \to \neg A$ est un théorème intuitionniste (on déduit facilement $\neg A$ de $\neg B$ et $A\to B$, remarquer que $\neg X$ est toujours équivalente à $X\to \perp$, voire en est considérée comme une abréviation chez certains auteurs ).

Conique · October 2017

Bonsoir,

Je me permets de m'immiscer sur la pointe des pieds dans cette discussion, car j'avais déjà réagi un peu plus haut et que de l'eau a coulé sous les ponts, semble-t-il.
Je tenais à préciser à @remark et à @christophe c que je ne leur faisait absolument aucun reproche personnel, et que je m'étais excusé de m'être un peu emporté un soir tard, après une journée un peu difficile (je vois que @remark a effacé tous ses messages, j'espère que ce n'est pas à cause de moi !).

J'avais entendu parler de Coq, ça m'a donné l'envie d'aller voir ce que c'était, merci @Foys.
Une chose m'interpelle tout de même dans ce qui est dit au-dessus. Pour moi, il n'y a de contraposée que d'une implication. Ainsi, l'expression La contraposée de A n'a pas de sens a priori (sauf si A, a posteriori, se révèle être une implication).

Ensuite, la preuve par l'absurde, dans mes souvenirs, mène à une absurdité logique : à une expression logiquement fausse. C'est là ce qui la distingue de toutes les autres preuves. Or, $(\neg B \rightarrow \neg A)\rightarrow (A \rightarrow

$ est vraie, et c'est, pour moi, ce qu'on appelle le raisonnement par contraposition : au lieu de montrer $(A \rightarrow

$, on utilise l'équivalence logique entre une implication et sa contraposée et on prouve $(\neg B \rightarrow \neg A)$ à la place. En effet, une implication est vraie si et seulement si sa contraposée l'est.

Je ne vois donc pas en quoi la preuve du professeur était une preuve par l'absurde, dans la mesure où aucune absurdité n'était levée.
Avec mes excuses si mon discours manque de clarté, et avec mes remerciements si quelques éclaircissements pouvaient être apportés (sans toutefois consommer temps et énergie inutilement, un lien vers une lecture suffirait sûrement).

pldx1 · October 2017

Bonjour.
Il y a des logiques qui pratiquent le tiers exclus (pour toute proposition $A$ on a $\neg \neg A=A$), et il y en a d'autres.
Et alors, il est intéressant d'avoir des notations qui indiquent la logique dans laquelle on est en train de calculer. L'usage (général) est d'utiliser $\implies$ pour la déduction en logique classique, définissant $A\implies B$ par $\neg A \; ou\;B$. Tandis qu'il est d'usage de noter $A \to B$ la déductibilité dans une autre logique (la propriété: si j'ai une preuve de $A$, je sais construire une preuve de $B$).

On a alors$\def\To{\;\longrightarrow\;}$ $$\begin{cases} \left(A\implies B\right)\implies \left(\neg B\implies \neg A \right) \\
\left(A\To B\right)\To \left(\neg B\To \neg A \right)

\end{cases}$$ Autrement dit, l'implication contraposée se déduit de l'implication directe (pour les deux logiques). Une preuve par contraposition consiste à prouver la contraposée... et à utiliser le tiers exclus. En l'absence de la propriété de tiers exclus, on se retrouverait bloqué à l'étape: $\left(\neg B\to \neg A\right)\to \left(\neg \neg A\to \neg \neg B \right)$, sans pouvoir revenir à $\left(A \to B \right)$

D'ailleurs, Foys a montré qu'il y a équivalence entre supposer le tiers exclus et supposer que toute implication directe se déduit de sa contraposée.

Cordialement, Pierre.

Conique · October 2017

Merci pour cette explication, c'est on ne peut plus clair !

Sincères salutations.

Post Scriptum.
Je tombe ce matin même sur un énoncé en lien avec le sujet. C'est de la logique classique, un énoncé du à un non mathématicien du nom de Wason en 1960. Cela peut en amuser certains (@crikacrika notamment)
Énoncé :Soient 4 cartes portant chacune un chiffre sur une face et une lettre sur l'autre.
Elles sont posées à plat, avec les faces visibles suivantes : $A$, $K$, $2$, $7$.
Consigne : sélectionner la ou les carte(s), en nombre minimal, qu'il est nécessaire de retourner pour tester l'hypothèse suivante : Toute carte qui a un $A$ sur une face a un $7$ sur l'autre face.

GaBuZoMeu · October 2017

pldx1 écrivait:

> L'usage (général)
> est d'utiliser $\implies$ pour la déduction en
> logique classique, définissant $A\implies B$ par
> $\neg A \; ou\;B$. Tandis qu'il est d'usage de
> noter $A \to B$ la déductibilité dans une autre
> logique (la propriété: si j'ai une preuve de
> $A$, je sais construire une preuve de $B$).

Ga ? je ne sais pas où tu as vu jouer ça, pldx.

J'écrirais plutôt, avec le formalisme du calcul des séquents (LK pour le classique et LJ pour l'intuitionniste) :
$\neg B \to \neg A \vdash_{\mathrm{LK}} A \to B$, mais $\neg B \to \neg A \not\vdash_{\mathrm{LJ}} A \to B$.

pldx1 · October 2017

Bonjour GaBuZoMeu.

Quelle notation préconises-tu lorsque l'on veut écrire que l'on n'est absolument pas en train de faire un
calcul de séquents, mais simplement en train de calculer des booléens avec des tables de vérité ?

Cordialement, Pierre.

GaBuZoMeu · October 2017

Tu ne me dis pas où tu as vu jouer qu'on écrit $\implies$ en logique classique et $\to$ en logique intuitionniste.
Calculer des booléens avec des tables de vérité en logique propositionnelle intuitionniste, j'avoue que ça me laisse perplexe.

pldx1 · October 2017

Calculer des booléens avec des tables de vérité en logique propositionnelle intuitionniste, j'avoue que, moi aussi, cela me laisserait perplexe. Par conséquent, il s'agit de calculer avec des tables de vérité dans la logique rantanplan, dite classique.

Cela dit, j'ai beaucoup trop vu de textes écrits de façon ambigüe, où l'on met un certain temps avant de deviner quelle est la logique utilisée. Si tu préfères dire l'une pour la déduction, l'autre pour l'implication, cela me va aussi.

GaBuZoMeu · October 2017

Si tu préfères dire l'une pour la déduction, l'autre pour l'implication, cela me va aussi.

Euh ... pas compris. Mais ça ne vaut pas la peine d'expliquer, à mon avis.

Problèmes de logique

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 18