P implique antitruc

Martial · November 2019

Bonsoir,
J'ouvre un fil qui est très connexe avec celui sur le RPA, mais je ne veux pas polluer ce dernier avec des questions spécifiques et personnelles.
A noter que je m'adresse à Christophe, mais bien entendu tous les intervenants peuvent intervenir (pléonasme).

Quand j'ai acheté le livre de Pierre Ageron (2002 ? 2003 ? 2004 ?) et que j'ai découvert qu'on n'utilisait pas RPA pour prouver l'irrationalité de racine de 2, j'y ai cru à moitié. Quand tu as commencé à pousser des gueulantes répétitives sur le forum à propos des profs ou des auteurs qui prétendaient que RPA était nécessaire dans ce théorème, j'ai commencé à y croire aux 3/4. Depuis que tu m'as tout bien expliqué, j'y crois à 100°/°.
Problème : pendant des années j'ai expliqué le RPA à mes élèves (ou étudiants) de la façon suivante : Monsieur X est accusé du meurtre de Madame Y, survenu le 18 décembre 2029 entre 16h et 20h selon les estimations du légiste, dans une ville de France métropolitaine nommée Sarcelles-Plage. Lors du procès, l'avocat de la défense explique, preuves à l'appui, qu'à cette période M.X était en vacances à Honolulu. Le juge, qui est un bon logicien, en déduit que (M.X est coupable du meurtre) implique (M.X a le don d'ubiquité), ce qui est absurde. La cour en déduit que M.X est innocent, i.e. que non (M.X a tué Mme Y).
Je réalise maintenant que ce raisonnement n'est pas du RPA mais tout simplement l'expression du fait que P implique antitruc est équivalent à non P.
D'où mes questions :
1) Comment justifies-tu cela ? Considères-tu non P comme un raccourci pour P implique antitruc, ou bien vois-tu cela comme une espèce de principe philosophique censé être accepté par l'ensemble de la communauté mathématique internationale ?
2) (plus difficile) : Comment expliquer le VRAI RPA à des étudiants, disons de Terminale S ou de 1ère année de supérieur ?
Je veux dire : si on leur explique ça par non non P implique P, on va finir tous les deux dans le même asile. Certes ça nous permettra d'avoir de grandes discussions philosophiques, mais ça sera quand même moins sympa que l'apéro dont parlait Dom dans le précédent fil, lol

Maxtimax · November 2019

L'exemple que tu donnes relève de la contraposée, pas du RPA : tu dis que $P\to Q$ donc $(Q\to C) \to (P\to C)$, puis tu l'appliques à $C = \bot$.
Le premier est une "évidence" : supposons $Q\to C$, supposons $P$. Alors $Q$. Alors $C$.
Le second te donne, avec $\neg P = (P\to \bot)$, que $\neg Q \to \neg P$ : c'est le principe de contraposée (ensuite tu dis que ton juge sait que $\neg Q$ parce qu'il est raisonnable, et il en déduit $\neg P$ par modus ponens; pas de RPA dans l'affaire)

Pour illustrer le RPA tu veux illustrer $\neg \neg P \to P$.
Dans ton exemple, puisque tu définis "est innocent" par une négation ("n'a pas tué") tu ne peux pas utiliser ça en tant que $P$.
Par exemple, disons que la personne qui prosécute prouve que X et Y étaient complètement isolées de tout le monde, dans un chalet, et prouve que personne n'était avec eux; puis prouve (trop forte !) que ce n'était ni un suicide, ni un accident (Y a 3 balles dans le dos ou je ne sais quoi)
Remarque que ça ne constitue pas une preuve directe que X a tué Y : rien de tout ça ne dit qu'on a retrouvé les empreintes de X quelque part, qu'on a un témoin, une preuce vidéi ou qu'on a un motif de meurtre ou quoi que ce soit : il n'y a pas de preuve directe que c'est X qui l'a fait
Mais si X n'a pas tué Y, alors Y n'est pas morte (pas de suicide, pas d'accident, et personne d'autre dans le chalet). Ça c'est absurde : donc non (X n'a pas tué Y). Donc X a tué Y.

(J'ai fait du mieux que j'ai pu en restant dans ton exemple :-D)

Martial · November 2019

@Max : oui, je vois à peu près.
Je vais réfléchir à tout ça dès que j'aurai réussi à me passer le mal de crâne.
Merci et bonne journée à toi.
Martial

Foys · November 2019

@Martial,
Pour tout le monde, sauf les logiciens qui étudient spécifiquement ces sujets, il va de soi que la négation exprime un "contraire" et est involutive, autrement dit $\neg \neg X$ est équivalent à $X$ (voire est considéré comme égal).

Il a été découvert au XXième siècle qu'il n'est pas vrai que ça va de soi et qu'en supprimant des règles (une seule dans certaines présentations) de démonstration, on perdait l'implication $(\neg \neg X) \Rightarrow X$ et le caractère involutif de la négation.

Donc $(\neg F \Rightarrow \perp) \Rightarrow F$ (i)n'est pas un cas particulier de $(Y \Rightarrow \perp) \Rightarrow \neg Y$ (ii). Il faut mettre à contribution un axiome supplémentaire pour déduire (i) de (ii) (par exemple passer par $\neg \neg X \Rightarrow X$ ou -ça revient in fine au même- $X \vee \neg X$ i.e. le "tiers exclu" ).

Ce sont les constructions de type (i) et elles seules qui portent le nom de "raisonnement par l'absurde".
Quand on les formalise, les preuves habituelles de "$\sqrt 2$ est irrationnel", "l'ensemble des nombres premiers est infini" ne les utilisent pas.

Pour info, ces théorèmes sont prouvables en COQ avec tout par défaut (il n'admet pas le raisonnement par l'absurde qui doit être rajouté manuellement dans les hypothèses).

Foys · November 2019

La logique intuitionniste est équivalente à (et peut être assimilée à) une logique où il n'y a aucun symbole de négation et où il y a une formule spéciale notée $\perp$ qui signifie littéralement "tout est vrai" (i.e. dans les axiomes il y a $\perp \Rightarrow P$ pour tout énoncé $P$).

Ainsi on ne voit plus au nom de quoi on peut déduire $A \Rightarrow B$ de $(B \Rightarrow \perp) \Rightarrow (A \Rightarrow \perp)$

En l'espèce $\neg X$ est alors une abréviation pour $X \Rightarrow \perp$ et ne signifie plus vraiment le "contraire" de $X$.