Non raisonnement par l'absurde

Système

Cette discussion a été créée à partir de réponses séparées de : Maths pour les élèves qui rentrent en prépas.

Dom

La description avant les exemples est bonne. 

On commence par nier la conclusion.
Mais ici, je ne vois pas une quelconque référence à une négation. Je cherche un « ne », un « pas », etc. et je n’en vois pas. 

Définition : irrationnel = non(rationnel)

1) Pour commencer un raisonnement par l’absurde, donc pour commencer en supposant que « irrationnel est faux » :  

Ça devrait commencer par « si ce n’est pas irrationnel » et non pas par « si c’est rationnel ». 

Autrement dit :  

Ça devrait commencer par « si non(non(rationnel) » et non pas par « si rationnel ». 

2) Ensuite dire « si ce n’est pas irrationnel, alors c’est rationnel » serait déjà utiliser le raisonnement par l’absurde (i.e.: non(non(rationnel) donc rationnel).

Admettre  « non(non(.) » donc « (.) » c’est utiliser un raisonnement par l’absurde. 

3) Peut-être est-ce ce qui est fait dans la tête de l’auteur mais ce n’est pas rédigé du tout DONC ce n’est pas un raisonnement par l’absurde qui est rédigé.

Sur ce qui est fait : là, ça commence par « si rationnel » puis ça aboutit à une contradiction. 

Ça montre SANS raisonnement par l’absurde que c’est « non(rationnel) ».

Faux amis : quand on déduit un truc absurde, ça ne signifie pas forcément que l’on a effectué un raisonnement par l’absurde.  

Je m’arrête là.
Poursuivre un fil existant ou en rouvrir un autre. 

JLapin

@Dom
Je suis d'accord avec tout ça mais ce n'est pas vraiment indispensable de proposer cette critique pour un poly de transition Terminale - supérieur à moins que l'objectif ne soit de nourrir le fil de discussion

Dom

Non, non, un éclairage, comme je l’ai dit.

xax

C'est surprenant, même la définition du raisonnement par l'absurde donnée ne me parait pas géniale. Pourtant à ce niveau "pour montrer que la proposition P est vraie, on suppose que non(P) est vraie et l'on en déduit une absurdité" me paraîtrait plus clair.

Positif

Ce sont peut être des considérations $\varphi$-losophique. On peut supposer qu’une chose est fausse, c’est notre propension à douter mais on ne peut pas concevoir qu’une chose fausse soit vraie, c’est contre la logique.

Dom

Je veux bien demander à la modération de raccrocher tous les messages concernant le thème « attention au RPA » à un autre fil ou d’en créer un nouveau. 

En effet, le fil est plutôt pour proposer des exercices à des lycéens et, je l’admets, ma remarque l’a rendu plus « technique » qu’ « informatif ». 

Il me semble que tous les autres messages peuvent y rester. Notamment les remarques, voire critiques sur les exercices en tant que tel.

john_john

Je comprends à présent d'où viennent les résultats lamentables du lycée LLG ! Si on les convainc que $x$ est rationnel est équivalent à $x$ n'est pas irrationnel...

Foys

La notion de raisonnement ne fait pas appel à la notion de vérité. Soit $H$ un ensemble quelconque de phrases (écrites avec les symboles usuels).

Une preuve dans $H$ est une suite finie d'énoncés $(A_i)_{1 \leq i \leq n}$ telle que pour tout $p\in \{1,...,n \}$, $A_p\in H$, ou bien il existe $q,r<p$ tels que $A_r = A_q \to A_p$.

On dit qu'un énoncé $X$ est un théorème de $H$ s'il existe une preuve $(B_i)_{1\leq i \leq m}$ dans $H$ telle que $B_m = X$.

I) On suppose que $H$ contient tous les énoncés de l'une des formes suivantes: $A \to (B \to A)$; $(A \to B \to C) \to ((A \to B ) \to (A \to C) )$. Alors: 

I.1°) étant donné un énoncé $X$, $X\to X$ est un théorème de $H$. Une preuve en est la suite:

$ (X \to (X \to X)\to X) \to ((X \to (X \to X)) \to (X \to X))$

$ X \to ((X \to X) \to X)$

$ (X \to (X \to X)) \to (X \to X)$

$ X \to (X \to X)$

$X \to X$

I.2°) Il est possible pour tous énoncés $P,Q$, de transformer algorithmiquement une preuve de $Q$ dans $H \cup \{P\}$ en une preuve de $P \to Q$ dans $H$ ("théorème de déduction").

En effet considérons une preuve quelconque $A_1,...,A_n$ dans $H \cup \{P\}$; on procède par induction sur $n$ pour construire une preuve $B_1,...,B_r$ dans $H$ telle que pour tout $i\in \{1,...,n\}$, il existe $s_i \in \{1,...,r\}$ tel que $B_{s_i} = P \to A_i$, de la façon suivante:

(i): si la liste est vide on renvoie la liste vide (la listes vide est une preuve dans la définition ci-dessus, elle ne prouve rien cela dit).

(ii) Si $n=m+1$, soit $L:=C_1,...,C_t$ la preuve obtenue par l'algorithme à partir de la liste $A_1,...,A_m$. trois cas se présentent:

**(ii) (a) $Q\in H\cup \{P\}$ car $Q\in H$; on concatène à $L$ la liste $A_{m+1};A_{m+1} \to (P \to A_{m+1});P \to A_{m+1}$

**(ii)(b) si $Q \in P \cup H$ parce que $Q=P$; on concatène à $L$ la liste obtenue en remplaçant $X$ par $P$ dans preuve de $X\to X$ dans I.1°).

**(ii) (c) il existe $p,q<m+1$ tels que $A_q = A_p \to A_{m+1}$. On concatène à $L$ la liste

$(P \to (A_p \to A_{m+1})) \to ((P \to A_p) \to (P \to A_{m+1})); (P \to A_p) \to (P \to A_{m+1}); P \to A_{m+1}$.

Le fait que cet algorithme fasse ce qui est annoncé est évident par récurrence sur la taille de la preuve. Exo: prendre votre langage préféré et implémenter cette procédure.

Le théorème de déduction permet de faire des raisonnements par ajout d'hypothèses, par exemple montrons que $(A \to (B \to C)) \to (B \to (A \to C))$. Il suffit pour cela de construire:

une preuve de $B \to (A \to C)$ dans $H \cup \{A \to (B \to C)\}$; il suffit pour cela de construire une preuve de $A \to C$ dans$H \cup \{A \to (B \to C), B\}$; et finalement il suffit de construire pour cela une preuve de $C$  dans $H \cup \{A \to (B \to C), B, A\}$. Or eci est très facile, il suffit de prendre la liste $A; A\to (B \to C); B \to C; B ; C$.

Il est vital de comprendre que étant donné un énoncé $M$ "supposer $M$" ne veut pas dire "se forcer solennellement à croire que $M$ est vrai". Supposer veut dire froidement: appliquer un programme informatique !! En l'espèce, le programme ci-dessus en ajoutant $M$ à $H$, pour plus tard obtenir un résultat du type $M \to N$ où $N$ est un autre énoncé.

Les énoncés qui peuvent être ajoutés successivement à $H$ afin d'appliquer le théorème de déduction sont arbitraires. Le psychodrame d'une prétendue impossibilité où même gêne à supposer des énoncés faux ne repose que sur une méconnaissance de ce qu'est une preuve. Espérons que le présent texte corrige cela.

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

II) Négations: 

On suppose qu'en plus des énoncés décrits au I), $H$ contient tous les énoncés de la forme suivante: $(\neg A \to B ) \to ((\neg A \to \neg B ) \to A)$.

Soit $W,X$ deux énoncés. Alors à l'aide d'une preuve de $X$ et d'une preuve de $\neg X$ dans $H \cup \{\neg W\}$, il est possible de construire une preuve de $W$ dans $H$. En effet, le théorème de déduction construit une preuves $\pi_1$ de $\neg W \to X$ dans $H$ ainsi qu'une preuve $\pi_2$ de $\neg W \to \neg X$ dans $H$ et la concaténation de $\pi_1,\pi_2$ et de $(\neg W \to X) \to ((\neg W \to \neg X) \to W); (\neg W \to \neg X) \to W; W$ fournit la preuve cherchée.

On dit qu'on fait un "raisonnement par l'absurde " lorsqu'on applique le programme informatique précédent pour prouver $W$

################################################

III) "Sens" des formules et vérité:

A aucun moment la construction ci-dessus ne fait référence à une quelconque notion de vérité. Désormais

on suppose qu'il existe un ensemble à deux éléments $\{vrai, faux\}$ et une fonction $f$ de l'ensemble des énoncés dans $\{vrai,faux\}$ qui est telle que pour tous énoncés $A,B$, si $f(A) = vrai$ et si $f(A \to B ) = vrai$, alors $f(B ) = vrai$. Soit $T$ un ensemble d'énoncés. Soit $L$ une preuve dans $T$.

Alors il est immédiat par induction sur la longueur de $L$ que si pour tout énoncé $X$ de $T$ on a $f(X)=vrai$, alors on a également $f(Y)=vrai$ pour tout énoncé figurant dans $L$ et en particulier, pour tout théorème de $T$ (théorème de correction).

Ces considérations sont conséquences de la définition de preuve données en préambule et sont essentiellement indépendantes de I) et II). A aucun moment la notion de "vérité" n'est mise à contribution pour construire des formes de raisonnements tels que celes abordées dans ces paragraphes.

NB: dans ce paragraphe le choix particulier de $\{vrai,faux\}$ pour interpréter les formules n'a été retenu que pour exposer une situation familière (le fait que tous les éléments de $H$ évoqués aux paragraphes I et II soient vrais est crédible). Il existe d'autres ensembles adaptés à d'autre choix d'ensembles d'énoncés de base (pour des logiques intuitionnistes, linéaires, sous-structurelles etc).

Vassillia

Bonjour, histoire de ne pas traumatiser les lycéens qui voudraient s'entrainer, Dom fait la distinction entre :

- réfutation : on suppose P et on déduit une absurdité donc on a démontré que non(P) est vraie

Ex : on suppose $\sqrt{2} \in \mathbb{Q}$ ...

- raisonnement par l'absurde : on suppose non(P) et on déduit une absurdité donc on a démontré que non(non(P)) est vraie donc P est vraie

Ex : on suppose $\sqrt{2} \notin \mathbb{R}\backslash\ \mathbb{Q}$ ... (on voit bien que c'est une mauvaise idée de partir comme ça)

 

Pourquoi faire cette distinction ? Car en logique intuitionniste, on a confisqué les axiomes qui permettent d'écrire la conclusion en gras.

Mais en logique classique, celle qu'utilise tout le monde en dehors de masters très spécialisés, on ne fait pas la distinction ni en prépa ni à la fac donc pas de panique et on n'est même pas obligé d'écrire cette étape non(non(P)) et personne ne sanctionnera.

Édit : j'ai écrit ce message avant le découpage par la modération, il n'a plus beaucoup d'intérêt maintenant mais je le laisse quand même 

Système

Cette discussion a été créée à partir de réponses séparées de : Maths pour les élèves qui rentrent en prépas.

Thierry Poma

Nous devions être deux sur le problème. Peu importe. Je vous invite à poursuivre ici-même pour discuter de vrais raisonnements par l'absurde et de faux raisonnement par l'absurde.

Que dire de la démonstration du théorème de Brouwer ?

Dom

Merci beaucoup, c’est de ma faute…
(peut-être peut-on déplacer aussi le message de Chaurien, et celui de xax, ici). 

En fait, comme je voulais répondre à Vassillia (voir tes mp 😀) : c’est de dire « je fais un raisonnement par l’absurde » et de ne pas le faire que je dénonce. 

Je dénonce nullement apprendre à des étudiants que « non(non(truc) » est équivalent à « truc ». 

Ça c’est évidemment ce qu’il faut faire : « on accepte l’idée que non(non(…)) ça revient à (…), et vous verrez peut-être plus tard que parfois on ne l’accepte pas ». 

On l’a bien vu dans les exemples dudit document. 

Aucune négation dans le début de la preuve. 

Je veux bien croire qu’elle est cachée dans la tête de l’auteur, peut-être par « évidence » mais je le souligne, c’est tout. 

À un lycéen qui fait ça, on peut lui demander « puisque tu fais un raisonnement par l’absurde, qu’est-ce que tu nies ? ». 

JLapin

Il te répondra probablement qu'en écrivant "supposons $\sqrt \in\Q$", il a nié le fait que $\sqrt 2$ soit irrationnel.

Vassillia

Je suis d'accord Dom, ce n'est pas stricto sensus un raisonnement par l'absurde mais on arrive quand même à une absurdité et on peut conclure grâce à cela, c'est un peu fourbe quand même au niveau du vocabulaire.

Je trouve aussi que tant qu'on ne comprend pas pourquoi non(non(P)) n'implique pas forcément P cela semble juste du formalisme un peu hors sol qui ne se rattache à rien de faire la distinction. Personnellement, je ne faisais pas vraiment la distinction entre partir de "P" et partir de "non(P)".

Je trouvais que c'était juste une lubie de logiciens avant que GaBuZoMeu m'explique comment on fait pour faire du calcul propositionnel intuitionniste à partir des valeurs de vérité qui sont des ouverts d'un espace topologique. Depuis d'accord, je rattache la distinction à quelque chose et cela a du sens pour moi.
J'avais essayé de me dépatouiller avec le calcul des séquents mais sans grand succès, c'est assez amusant mais pas très pratique selon moi.

Dom

Oui JLapin, s’il n’est pas de mauvaise foi, c’est ok. 

Première remarque : il a donc caché sa négation alors que c’est le début du début, c’est dommage. 

Deuxième remarque : s’il rédige comme ça, alors il peut même se vanter d’effectuer deux raisonnements par l’absurde dans la même démonstration. 

a) je suppose « $r$ non(non(rationnel) » DONC par RPA « $r$ rationnel ». 

b) j’ai supposé « $r$ non(non(rationnel)) » et j’ai trouvé un truc contradictoire donc j’en déduis « $r$ non(non(non(rationnel))) » et DONC par RPA « $r$ non(rationnel) ». 
C’est le jour où j’ai assimilé que la définition de la négation était « non(machin) signifie (machin => contradiction) » que j’ai compris les fils de ce genre. 

Vassillia

La bonne nouvelle, c'est que non(P) <=> non(non(non(P))) est vraie même en logique intuitionniste alors qu'on a seulement P => non(non(P)) en logique intuitionniste, c'est bien pensé cette histoire, faut pas croire. C'est pour ça que je ne me formalise pas sur l’appellation "raisonnement par l'absurde" ou non

Dom

On peut ranger ça dans la culture générale et dire à des étudiants qu’il n’est même pas utile d’utiliser l’expression « raisonnement par l’absurde ». 

C’est juste une histoire de sémantique. 

En fait je ne comprends pas la volonté de certains de continuer de le dire en sachant que c’est faux.
Sans arguments, on lit même « ce sont des trucs de logiciens » alors que ce n’est pas tout à fait le cas. 

Vassillia

En ce qui me concerne, c'est plutôt une volonté de ne pas embrouiller les lycéens inutilement.
Je n'utiliserai pas le terme sachant que c'est inadapté mais je ne corrigerai pas non plus un étudiant qui l'utilise, je ferai peut-être la remarque en coulisse à un collègue pas trop matheux par contre, ma pédagogie dépend très nettement du public

Foys

Je voudrais savoir pourquoi mon dernier message sur Gödel-Gentzen et le théorème de Brouwer, a disparu. S'il s'agit d'une mauvaise manipulation de mon côté (ce qui est possible), je m'excuse pour ce message.

Cordialement.

Dom

Dans ce fil « RPA ou pas » ? Ça ne me dit rien mais je n’étais pas là tout le temps…

Foys

@Dom oui, je l'ai rédigé après le déplacement des messages.

Thierry Poma

@Foys : bonsoir. Aucune mauvaise manipulation n'a été effectuée de la part de la modération. Je viens de le vérifier.

Dom

Parfois pendant le transfert d’un fil vers un autre j’ai perdu des messages. C’est peut-être le cas, hélas…

Georges Abitbol

@Vassillia : Personne n’ « utilise » la logique classique ou intuitionniste. Il n’y a que des démonstrations (et le niveau d’études en logique de la personne qui l’a rédigée n’a rien à voir là-dedans, pas plus que ses positions philosophiques). Chaque démonstration a des hypothèses. Certaines hypothèses font partie d’une liste qui s’appelle « logique intuitionniste », d’autres d’une liste qui s’appelle « logique classique », etc. La vraie raison pour laquelle des étudiants et étudiantes en prépa ne devraient pas s’inquiéter de ça, ce n’est pas que le problème soulève des subtilités logiques, c’est juste que personne ne s’attend à ce qu’ils et elles connaissent les différences entre ces listes. Par contre, les personnes chargées d’enseigner ça n’ont aucune excuse : si elles refusent d’apprendre ces listes, c’est par paresse.

Foys

D'accord, merci @Thierry Poma.

GaBuZoMeu

"Chaque démonstration a des hypothèses. Certaines hypothèses font partie d’une liste qui s’appelle « logique intuitionniste », d’autres d’une liste qui s’appelle « logique classique », etc. "

Pas trop d'accord avec cette présentation : pour moi, les règles de déduction ne sont pas des hypothèses.

Foys

GaBuZoMeu a dit :

Pas trop d'accord avec cette présentation : pour moi, les règles de déduction ne sont pas des hypothèses.

Les règles de déduction d'un système de preuve sont largement arbitraires elles aussi, on peut garder le modus ponens comme seule règle et faire passer tout le reste dans les axiomes, au prix de lourdeurs certes.

Georges Abitbol

Pour moi, une démonstration est un procédé qui amène le sceptique d’une conclusion à trouver une hypothèse dont il doit douter. Le sceptique a bien le droit de douter des règles de déduction !

A mon avis, les règles de déduction et les autres hypothèses ne sont pas opérationnellement discernables, et que c’est de la philosophie que de vouloir les distinguer. En l’occurrence, quand dans un texte, on écrit « or non(non(truc)) implique truc » ou « or $x$ est supposé positif par l’énoncé », je ne vois pas de différence substantielle.

GaBuZoMeu

Non, ce n'est pas de la philosophie. Les règles de déduction donnent les modes de fonctionnement des connecteurs et quantificateurs logiques. Le "non(non(truc)) implique truc" est un point important du fonctionnement du connecteur "non" en logique classique. Ce n'est pas du tout de même nature que "x est supposé positif".

Médiat_Suprème

Je suis d'accord avec GaBuZoMeu, le mot hypothèse ne me paraît pas idoine (pinaillage, je le reconnais), il y a d'une part les règles de la logique (construction des formules, règles de déduction, etc.), qui sont bien arbitraires comme le dit Foys et d'autre part les axiomes constitutifs d'une théorie. C'est une façon de distinguer Tautologies et théorèmes, c'est aussi le moyen pour que la logique soit un sujet d'étude (ce qui peut laisser les mathématiciens indifférents).

Et j'ajoute un deuxième bémol au message de Georges Abitbol, pour certains, le choix de travailler avec la logique intuitionniste est un choix philosophique

nicolas.patrois

Tu as parfaitement le droit de proposer des règles contradictoires. Le problème, c’est que pas grand monde ne te suivra (ou alors sur shtam) et que ce n’est pas très fécond.

Dom

J’ai compris l’utilisation de « hypothèse » par Georges dans le sens courant « ce que l’on accepte ». Je ne suis pas assez au fait de cette sémantiquement là (hypothèse, axiome, « règles acceptées ou utilisées »). 

Sur le fond je pense en effet qu’un enseignant doit se mettre à jour. Ces sujets ne sont pas shtamesques ni farfelus. 

Dire « j’utilise un raisonnement par récurrence donc 1+1=2 » pose un problème. 

Autant que de dire « j’utilise un raisonnement par l’absurde » sans évoquer la négation (évidente ou non). 

GaBuZoMeu

L'arbitraire des règles de déduction me semble en grande partie une fable.

Dom

Mince. J’avoue ne pas comprendre. 

Ne choisit-on pas les règles ? (on = l’humain)

Ou alors tu dis tout simplement qu’on ne choisit pas les règles n’importe comment ? (L’arbitraire n’est pas vraiment arbitraire)

Médiat_Suprème

"Arbitraire" ne doit pas être pris ici au sens de "n'importe quoi", mais au sens de "n'est pas imposé" par une observation (comme en physique), mais on peut penser qu'elles sont imposées (même s'il y a plusieurs jeux de règles) par la façon dont le cerveau humain fonctionne.

Foys

Le simple fait qu'une même logique puisse avoir plusieurs jeux de règles d'inférence différents (calcul des séquents/calcul des séquents sans coupure/déduction naturelle/système de Hilbert; pour les logiques intuitionnistes/classiques) fait que l'emploi de l'un ou l'autre de ces jeux de règles d'inférence est un choix (dicté par des considérations pratiques certes, écrire un assistant de preuve lisible et prouver le théorème d'Herbrand sont deux projets distincts pour lesquel certains choix seront plus appropriés). Comme tous les choix, ce choix est bel et bien arbitraire.

D'autre part même les règles que tout le monde considérait comme infaillibles se sont révélées contestables. Brouwer a dû beaucoup passer pour un imbécile à son époque. Plus tard, lorsque l'intuitionnisme a cessé d'être sulfureux, Girard a montré que les règles $\Gamma, A,A \vdash B \Rightarrow \Gamma, A \vdash B$ et $\Gamma \vdash B \Rightarrow \Gamma, A \vdash B$ pouvaient être refusées elles aussi, fournissant la logique linéaire (les phrases suivantes disent-elles la même chose ? "si j'ai 100 euros, je peux acheter un portable à 200 euros"; "si j'ai 100 euros et 100 euros je peux acheter un portable à 200 euros" et enfin "si j'ai 100 euros et 100 euros et une amende de 5000 euros, je peux acheter un portable à 200 euros").

Ce sont les résultats produits par ces règles et non les règles elles-mêmes qui ne sont pas arbitraires.

La reconnaissance du caractère arbitraire des règles inciterait aussi enfin les auteurs à rendre accessibles les règles qu'ils emploient au lieu de reprocher à leur public de ne pas les deviner intuitivement.

Médiat_Suprème

Et on n'a pas encore parlé des logiques modales

Ce qui me semble très important à enseigner aux étudiants, c'est la variété des logiques existantes, la logique classique du premier ordre n'est pas la seule à avoir droit de cité.

Dom

Je répète Vassillia :
-> l’étudiant n’en a pas besoin, ok !
-> mais qu’il écrive « j’ai raisonné par l’absurde »
alors que ce n’est pas le cas, non !
-> pire, que le prof le sache mais continue de l’encourager à écrire des choses erronées, non !
-> si le prof ne le sait pas, là, j’admets qu’il n’y peut rien. 

Vassillia

C'est mon coté pragmatique Dom, sachant que de nombreux profs feront l'erreur aussi, je ferme les yeux sur les erreurs des étudiants sans faire l'erreur moi-même autant que faire se peut sinon on se contredit et plus rien ne va. Mais du coup je suis d'accord que les profs devraient avoir une meilleure formation en logique, de toute façon, il faut toujours commencer par former les profs avant les étudiants, cela me semble logique (je laisse les logiciens choisir la logique la plus adaptée pour convaincre )

GaBuZoMeu

"Comme tous les choix, ce choix est bel et bien arbitraire."

Axiome de Foys : tout choix est arbitraire. Est-ce que cet axiome est arbitraire ?

Thierry Poma

Selon Jacques Duparc, voici la règle de l'absurdité classique :

Thierry Poma

A ne surtout pas confondre avec celle-ci, que l'on utilise souvent :

Affirmer $\neg{}\phi$, c'est avoir constaté que $\phi$ conduit à une contradiction. Règle utilisable en logique intuitionniste, me semble-t-il.

Thierry Poma

Enfin, voici la règle de l'absurdité intuitionniste, même si j'ai du mal à voir clairement :

En gros, si le système $\Gamma$ conduit à une contradiction, alors l'on peut déduire ce que l'on veut de ce système. Mais, je me trompe peut-être.

Médiat_Suprème

Cette interprétation me paraît correcte

Thierry Poma

Médiat_Suprème : bonjour. Je te remercie. En fait, il me semble que c'est le fameux "Ex falso sequitur quodlibet" qui figurait dans la première version du livre d'algèbre de Michel Queysanne.

L'on se sert souvent de la deuxième règle pour établir l'irrationalité de $\sqrt{2}$, par exemple. Inutile de faire appel à la première règle, vrai RPA.

nicolas.patrois

Thierry Poma a dit :

En gros, si le système $\Gamma$ conduit à une contradiction, alors l'on peut déduire ce que l'on veut de ce système. Mais, je me trompe peut-être.

C’est le « faux implique tout » de Christophe.

Foys

nicolas.patrois a dit :

C’est le « faux implique tout » de Christophe.

En fait en logique intuitionniste $\perp$ signifie "tout est vrai" (dans les sémantiques de type algèbre de Heyting $\perp$ est toujours interprété comme le plus petit élément de l'ensemble ordonné envisagé $H$ où l'ordre indique la force des phrases). La négation va être définie indirectement par $\neg A := A \to \perp$. Du coup $\perp \to B$ est pour tout $B$ une lapalissade mais on ne voit plus trop pourquoi $(A\to \perp) \to \perp$ entraîne $A$.

Par exemple un nombre irrationnel est un nombre tel que s'il est rationnel alors tout est vrai.

Thierry Poma

Nous nous sommes considérablement éloignés du thème original de ce fil qu'il est souhaitable de conserver. J'ai donc supprimé toute intervention n'ayant aucun rapport avec ledit thème.

Médiat_Suprème

On peut même remarquer que les Américains (Anglais ?) disent "all" pour lire $\perp$.

GaBuZoMeu

Ce qui peut être troublant puisque la valeur de vérité de $\bot$ dans le treillis des ouverts d'un espace topologique n'est pas le tout, mais le rien.