Raisonnement par l'absurde (RPA)

1)
J’en suis là :
En logique classique on montre facilement : P => non(non(P))
On dispose d’un axiome appelé RPA qui dit : non(non(P)) => P.
On a donc l’équivalence : P <=> non(non(P)).

Ma question : existe-t-il une logique où l’on déclare le non involutif ?
Mon préambule prouve que la logique classique le fait.

Mais alors pourquoi je pose la question ?
Quand les gens déclarent « pour moi, non(non(P)) <=> P », ils ne parlent jamais du RPA.
Ils parlent, en les torturant un peu, du Tiers Exclu.
J’ai compris qu’il s’agissait d’une logique équivalente à la logique classique.
Est-ce la « logique naïve » ?
C’est exactement le thème du début du message de Christophe : http://www.les-mathematiques.net/phorum/read.php?16,1880930,1880930#msg-1880930
Il parle de « niveau grossier », de « faute ».

2)
Est-ce que tout le monde définit « non » par « implique TOUT » ?
Est-ce un choix de chaque auteur ?
Est-ce d’habitude plutôt fait en LI ?

Tu dis que je déforme ton argument, puis tu répètes exactement le même. (:D

Pourquoi supposer $P$ pour démontrer $\bot$ et ainsi avoir une démonstration de $\neg P$ ?
Parce que la règle d'introduction du $\neg$ à droite est
$$\begin{array}{rcl} \Gamma, P&\vdash&\bot\\
\hline
\Gamma &\vdash&\neg P\end{array}$$
Ceci aussi bien en logique classique qu'en logique intuitionniste.
De même, pourquoi supposer $P$ pour démontrer $Q$ et ainsi avoir une démonstration de $P \Rightarrow Q$ ? Parce que que la règle d'introduction du $\Rightarrow$ à droite est
$$\begin{array}{rcl} \Gamma, P&\vdash&Q\\
\hline
\Gamma &\vdash& P\Rightarrow Q\end{array}$$

Même si on de définit pas $\neg P$ comme $P\Rightarrow \bot$, l'équivalence logique des deux se démontre aussi bien en logique intuitionniste qu'en logique classique.

Démontrer $\neg P$ en supposant $P$ pour en déduire l'absurde, c'est ce que tout le monde fait et c'est ce que formalisent les règles des systèmes de déduction conernant le $\neg$, qu'elles soient classiques ou intuitionnistes.

Ton baratin tourne complètement à vide, Ltav.

@Dom :
Pour le point 1), il y a beaucoup de questions.
Du point de vue strictement syntaxique, $non$ n'est jamais involutif. Par contre, dans toute démonstration, tu as le droit de supposer tout ce que tu veux, tu peux même utiliser $0 = 1$ (et dans ce cas, on ne devra pas objecter que ta démonstration est fausse, mais qu'on est platement d'accord avec toi : en supposant $0 = 1$, on peut démontrer n'importe quoi). Il y a donc des démonstrations qui supposent $non(non(P)) \Leftrightarrow P$, d'autres non.

Si une des hypothèses d'une démonstration est $non(non(P)) \Rightarrow P$, on dit qu'elle "utilise l'axiome $RPA$". Si une des hypothèses est $P \ ou \ non(P)$, on dit qu'elle "utilise le tiers-exclu". Tiers-exclu et $RPA$, c'est "plus ou moins la même chose", dans le sens où si on admet d'autres axiomes logiques moins "polémiques", on peut facilement démontrer qu'on démontre les mêmes choses avec l'un ou avec l'autre.

Bref, si quelqu'un te dit "je travaille en logique classique", il n'aura pas le droit de te faire des objections sur $non(non(P)) \Rightarrow P$ si tu l'utilises dans une démonstration. Si quelqu'un te dit "je travaille en logique intuitionniste", si tu lui montres une démonstration où tu utilises $non(non(P)) \Rightarrow P$, il te dira "ha ben oui, mais bon moi je refuse ça, a priori".

Pour le point 2), de deux choses l'une :
- soit on décide d'utiliser l'abréviation $non(P) := P \Rightarrow \bot$ ;
- soit on décide que pour toute suite de caractères $P$ que l'on considère comme un énoncé, alors $non(P)$ doit aussi être considéré comme un énoncé ; et dans ce cas, si on choisit d'admettre une série d'énoncés pas très polémiques qui disent de $non$ ce qu'on voudrait qu'il soit, alors on peut démontrer que, pour tout $P$, $non(P) \Leftrightarrow (P\Rightarrow \bot)$.

Exemple : acceptons que les choses suivantes sont des démonstrations acceptables :
- on a $P$ et on a $non(P)$, et donc $\bot$ ;
- sous l'ensemble d'hypothèses $\Gamma$, supposons de plus $B$, blablablabla et donc $C$ ; et donc, sous l'ensemble d'hypothèses $\Gamma$, on a démontré $B \Rightarrow C$.

Alors $non(P) \Rightarrow (P \Rightarrow \bot)$ !

De plus, si on accepte que la chose suivante est une démonstration acceptable :
- sous l'ensemble d'hypothèses $\Gamma$, et l'hypothèse additionnelle $P$, on a conclu précédemment que $\bot$ ; et donc, sous l'ensemble d'hypothèses $\Gamma$, nous pouvons conclure que $non(P)$.

Alors $(P\rightarrow \bot) \Rightarrow non(P)$.

EDIT : J'ai oublié de conclure ! Bref, il ne faut pas trop s'inquiéter de savoir si $non(P)$ est défini comme $P\Rightarrow \bot$ ou non, quitte à ajouter des axiomes pour dire comment on voudrait que $non$ se comporte.

Et, remarque : quand je dis "polémique", ça dépend de la polémique :-D Ici, ça doit s'entendre comme "polémique au sens intuitionniste vs classique".

@Gbzm : http://www.les-mathematiques.net/phorum/read.php?16,1880930,1888046#msg-1888046

Je ne peux pas m'absenter quelques heures sans te retrouver étaler ton incompréhension totale (à supposer qu'elle soit de bonne foi) de mon argument. Tu l'as bel et bien changé mais tu le réaliserais mieux si tu arrêtais de prendre tes contradicteurs pour des baratineurs ou pire des...(désolé de parler ainsi).

A nouveau, il ne s'agit pas de remettre en cause que pour démontrer $(P => Q)$, je doive par définition supposer P pour en déduire Q. C'est absolument clair et évident et tu fais bien du radotage mais purement hors-sujet. Ma question est pourquoi, pour démontrer R, dois-je utiliser systématiquement $(P => Q) => R$ (supposée vraie), au lieu de l'une des relations $(Q_i => Q) => R$, vraie également pour tout $i \in \mathbb{N}$, avec des propositions $Q_i$ toutes différentes de P ? Eh bien, soit on impose ce choix par convention, en posant par exemple $R := (P => Q)$ comme en logique intuitionniste, soit on le démontre, comme en logique classique lorsque l'on déduit puissamment du tiers-exclu que : pour tout entier $i$, $Q_i = P$, ce qui justifie parfaitement en LC pourquoi on suppose P plutôt que l'une des innombrables $Q_i$. Est-ce plus clair pour toi ?

Ltav, toujours aussi creux.

Et tu ne réponds pas à ma question, que je répète.

Quelle différence fais-tu entre "$P$ est fausse" et "$\neg P$ est vraie" ?? Du point de vue classique ? Du point de vue intuitionniste ?

Gbzm a écrit:

Ltav, toujours aussi creux.

Voilà enfin un contrargument "plein"...Puisque tu n'as rien d'autre à rétorquer, ce débat est donc clos entre nous deux.

Pour ta question, ces propositions sont bien sûr sémantiquement équivalentes. Leurs démonstrations toutefois impliquent des techniques différentes dont j'ai maintes fois parlé (*). Je te renvoie à mes posts précédents.

[small](*) Pour démontrer Q vraie, où Q = non P, je suppose non Q, i.e. P par tiers-exclu, je montre l'absurde, donc P est faux, i.e. Q est vraie : c'est le raisonnement par l'absurde, valable en LC. Il explique pourquoi je suppose P et aucune autre proposition. Pour démontrer P fausse, je suppose P, j'arrive à l'absurde, donc P fausse : c'est la réduction à l'absurde, valable aussi en LI.[/small]

Hum... « pointeur » est un vague mot... ça remonte (pour situer, DEUG MIAS, 1998, Turbo Pascal ou C++).

Mais vas-y, poste quand tu pourras, on sait être autodidacte de nos jours. On essaiera du moins.
Ça m’intrigue par contre, qu’est-ce que tu vas bien pouvoir me faire faire sur ce sujet ?

@Dom : Je ne suis pas sûr de ce que je vais dire, mais Christophe corrigera au besoin. Quand je disais, tout à l'heure, qu'il y avait différentes polémiques, c'est que le débat : "Est-ce que le RPA est un axiome qu'on veut dans nos maths ou non ?" a été fructueux car a suscité l'étude de la logique intuitionniste ; mais de nos jours, il y a d'autres débats, comme par exemple "Est-ce que si on suppose une hypothèse, cela va de soi que l'on peut l'utiliser plusieurs fois ?". Par exemple, pour citer Girard, si j'ai un euro, je peux acheter un café (à un euro) et je peux acheter un déca (à un euro), mais je ne peux pas acheter un café et un déca (puisque je n'ai qu'un euro). Ça donne lieu à d'autres logiques, etc. Et je crois que Christophe veut "te faire sentir" ce genre de problèmes.

@Cc : http://www.les-mathematiques.net/phorum/read.php?16,1880930,1888206#msg-1888206

Au lieu de juste ricaner et partir dans tous les sens, pourrais-tu s'il te plaît préciser ce que tu contestes et pourquoi tu le contestes (entre "délire", "faux", "$\mathbb{N}$ qui voulait passer des vacances tranquilles", etc. on ne s'y retrouve plus).

Nota bene: Depuis pas mal de temps, sauf exception, tu n'oses plus rentrer dans le détail des arguments et préfères te cacher derrière des pitreries "quasi-désespérées" du même genre. Il est vrai que quand tu acceptes (toi ou d'autres du même comportement) de jouer le jeu de l'échange scientifique rigoureux, ça donne presque toujours des choses comme

http://www.les-mathematiques.net/phorum/read.php?16,1886712,1888360#msg-1888360

J'attends le détail de tes objections. Merci.

Bonne nuit à tous.

@GaBuZoMeu : On calme le jeu ! :-D

Tu as raison Christophe, à la relecture j'ai sans doute mal formulé ma question. Il vaudrait mieux formuler comme ça, de façon plus neutre :
Dans le formalisme intuitionniste, quel rapport logique
- entre $\neg\exists x\ P$ et $\forall x\ \neg P$,
- entre $\neg\forall x\ P$ et $\exists x\ \neg P$ ?

En attendant, le tour de passe-passe toposique promis :

On se place dans le topos des faisceaux sur un espace topologique $X$. Dedans on a :

- un objet des nombres rationnels $\mathbb Q_X$, qui est le faiceau constant $\mathbb Q$. Ça veut dire que les sections de ce faiceau sur un ouvert $U$ de $X$ sont les fonctions localement constantes de $U$ dans $\mathbb Q$.

- un objet des nombres réels (de Dedekind) $\mathbb R_X$, qui est le faisceau des fonctions continues à valeurs réelles. Ça veut dire que les sections de ce faisceau sur un ouvert $U$ de $X$ sont les fonctions continues de $X$ dans $\mathbb R$.

Pas de panique donc, on travaille avec des objets bien rassurants : les fonctions localement constantes à valeur rationnelles, et les fonctions continues à valeurs réelles. On s'intéressera essentiellement aux sections globales (définies sur $X$), qu'on appellera "éléments" (bien que ce soit une très mauvaise idée de faire ça). Les "éléments" de $\mathbb R_X$ sont les fonctions continues $X\to \mathbb R$, et parmi elles les "éléments" de $\mathbb Q_X$ sont les fonctions localement constantes $X\to \mathbb Q$.

Prenons maintenant pour $X$ un espace bien sympathique : $X=\mathbb N\cup \{\infty\}$ le compactifié d'Alexandrov de $\mathbb N$ avec la topologie discrète. Rappelons que les voisinages de $\infty$ sont les complémentaires de parties finies de $\mathbb N$. Les "éléments" de $\mathbb R_X$ sont les couples $(u,\ell)$ où $u:\mathbb N\to \mathbb R$ est une suite réelle qui converge vers le réel $\ell$ ; parmi eux, les "éléments" de $\mathbb Q_X$ sont les $(u,\ell)$ où $u$ est une suite de nombres rationnels qui stationne à partir d'un certain rang, et $\ell$ la valeur rationnelle où $u$ stationne.

Si $(u,\ell)$ est un élément de $\mathbb R_X$, quelle est la valeur de vérité de la phrase "$(u,\ell)$ est rationnel". Une valeur de vérité, c'est un ouvert de $X$. L'intersection de la valeur de vérité de "$(u,\ell)$ est rationnel" avec $\mathbb N$ est l'ensemble des entiers naturels $n$ tels que $u(n)\in \mathbb Q$. Et $\infty$ appartient à cette valeur de vérité si et seulement si la suite $u$ stationne sur une valeur rationnelle à partir d'un certain rang.

Quelle est la valeur de vérité de "$(u,\ell)$ n'est pas rationnel" (ou "$(u,\ell)$ est irrationnel") ? La restriction de $(u,\ell)$ à tout ouvert contenu dans cette valeur de vérité n'a pas le droit d'être rationnelle ; la valeur de vérité de "$(u,\ell)$ est irrationnel" est l'intérieur du complémentaire de la valeur de vérité de "$(u,\ell)$ est rationnel". L'intersection de la valeur de vérité de "$(u,\ell)$ est irrationnel" avec $\mathbb N$ est l'ensemble des entiers naturels $n$ tels que $u(n)\not\in \mathbb Q$. Et $\infty$ appartient à cette valeur de vérité si et seulement si tous les $u(n)$ sont irrationnels à partir d'un certain rang.

Considérons l'élément de $\mathbb R_X$ donné par le développement décimal de $\sqrt2$ : $u=(1,1.4,1.41,1.414,\ldots)$ et $\ell=\sqrt 2$. Ce n'est pas un "élément" de $\mathbb Q_X$ : la valeur de vérité de "$(u,\ell)$ est rationnel" est $\mathbb N$, $\infty$ n'y appartient pas. Par contre, la valeur de vérité de "$(u,\ell)$ est irrationnel" est vide. Et par conséquent, la valeur de vérité de "$(u,\ell)$ n'est pas irrationnel" est tout $X$. Ceci montre que $\mathbb Q_X$ n'est pas non-non clos dans $\mathbb R_X$, contrairement à ce que j'aurais parié.

La raison de mon pari loupé : et si on était parti avec un espace $X$ localement connexe, au lieu de notre compactifié d'Alexandrov de $\mathbb N$ qui ne l'est pas ?

Je suis trop loin.
J’ai vu pour la dernière fois les catégories en 2002.
J’ai eu un module de maîtrise en « topologie algébrique » mais honnêtement je dois bien reconnaître que j’étais une bille, même en algèbre linéaire toute bête.
Je ne sais pas ce qu’est un topos (j’en ai lu un topo (:P)).
Les faisceaux, ça m’interpelle au niveau du vécu...

Bon, merci bien entendu, qui sait, j’arriverais peut-être à récoler les morceaux.

Je vais quand même aller voir ces objets...ça prendra du temps.

Haha.
Si j’en suis capable.
Mais la description de m’sieur GaBuZoMeu nous prend par la main...

À plus tard.

PS : faut rajouter un jour de WE en pleine semaine pour moi, mais je ne sais pas si c’est dans les tuyaux...

Oui, oui, ton descriptif (est-ce le bon mot ?) des objets est clair pour que je parvienne à m'investir :-).