Il y a une différence en général entre une proposition fausse et une proposition impliquant le faux ?
Une proposition qui serait ni vraie ni fausse pourrait impliquer le faux. D’où la nécessité de retirer le tiers exclus.
Banni
Mais c’est quoi une proposition « fausse » ? Il existe des formalismes dans lesquels $\lnot A$ n’est pas équivalent à $A \to \bot$ ?
Le point de vue de matheux c’est de dire qu’une proposition est fausse si tu peux exhiber un contre-exemple. Le point de vue de logicien, c’est de dire que la négation est prouvable.
Il existe des formalismes dans lesquels $\lnot A$ n’est pas équivalent à $A \to \bot$ ?
Tu pourrais avoir $A$ ni vraie ni fausse qui implique $\bot$. Et pourtant $\neg A$ ne peut pas être vraie. 
Une telle situation permet de dire que si $A$ est quelque chose, alors $A$ est fausse. Mais il manque l’étape pour montrer que $A$ est quelque chose.
Je pense que dans un cadre du type analyse non standard ça arrive à tours de bras. Mais mes souvenirs de lecture sont trop loin pour donner une référence claire.
Banni
Le point de vue de matheux c’est de dire qu’une proposition est fausse si tu peux exhiber un contre-exemple. Le point de vue de logicien, c’est de dire que la négation est prouvable.
Oui, donc je parlais du point de vue du logicien, et je demandais si tu avais un exemple de cadre formel où on n’a pas $(A \to \bot) \to \lnot A$.
Une telle situation permet de dire que si $A$ est quelque chose, alors $A$ est fausse. Mais il manque l’étape pour montrer que $A$ est quelque chose.
Je ne vois vraiment pas ce que ça veut dire formellement que « $A$ est quelque chose »… 
Pour que je puisse suivre la conversation blo yhg, tu peux expliquer les notations?
Je ne vois vraiment pas ce que ça veut dire formellement que « A est quelque chose »…
$A$ est vrai ou fausse (ce que j’ai appelé "quelque chose") si $A$ ou $\neg A$ a une preuve.
Pour que je puisse suivre la conversation blo ygh, tu peux expliquer les notations?
$\bot$ signifie "faux" (l’énoncé tautologiquement faux, du style $\forall x\, x\neq x$, modulo équivalence logique). $\neg A$ signifie non $A$. Et $A\rightarrow B$ signifie $A$ implique $B$. (C’est plus lisible si on remplace les $\implies$ par $\rightarrow$ vu qu’on a pas vraiment besoin de considérer des applications ici.)
D’accord, j’avais déjà rencontré l’énoncé faux dans tes derniers mp blo yhg, j’avais juste oublié, désolé.
En revanche, je lis "A \rightarrow B" comme une application de A dans B.
Dans un raisonnement par l’absurde, on est amenés à écrire une assertion fausse, ce qui n’est pas le cas lors d’un raisonnement par contraposée.
Ce n’est pas clair. Si tu retires le tiers exclus, tu peux montrer que machin implique le faux, mais tu peux pas en conclure que machin est une assertion fausse.
Et si tu retires pas le tiers exclus, il me semble que les deux procédures sont équivalentes.
Je ne sais pas. Mais en maths (i.e. pas en logique), classiquement on accepte le tiers-exclu, justement pour avoir le droit au raisonnement par l’absurde. En gros, l’exemple classique que j’avais en tête, c’est $\sqrt 2$ est irrationnel. Cet énoncé n’est pas une implication. Pour autant, lorsque l’on veut en faire la preuve, on nie l’assertion et on aboutit à une contradiction. Alors, certes, on peut reformuler l’énoncé artificiellement en disant par exemple : « Si $\sqrt2$ est irrationnel, alors toute fraction est réductible », mais il n’empêche que c’est un peu étrange de faire ça.
C’est un peu différent que de vouloir démontrer une implication, car pour montrer $A\rightarrow B$, il faut et il suffit de montrer $\neg B\rightarrow \neg A$. Ces deux assertions étant équivalentes, on n’écrit à aucun moment dans la preuve un énoncé faux, ce qui est structurellement d’un raisonnement par l’absurde. La pirouette consistant à reformuler une preuve par l’absurde en une implication dont la conclusion est fausse me semble un peu artificielle.
D’accord, j’avais déjà rencontré l’énoncé faux dans tes derniers mp blo yhg, j’avais juste oublié, désolé.
En revanche, je lis "A \rightarrow B" comme une application de A dans B.
Oui, effectivement dans le formalisme usuel et en maths « du quotidien » (i.e., là encore, pas en logique), la flèche $A\rightarrow B$ désigne une application de $A$ dans $B$. Mais en calcul propositionnel, on ne manipule pas tellement de fonctions, seulement des assertions avec leur valeur de vérité. Pour alléger les symboles, il est d’usage de remplacer $\Rightarrow$ par $\rightarrow$ dans ce contexte.
mais il n’empêche que c’est un peu étrange de faire ça.
La pirouette consistant à reformuler une preuve par l’absurde en une implication dont la conclusion est fausse me semble un peu artificielle.
Sauf que c’est ce qu’on fait en pratique :P. D’ailleurs je pense que ça se voit au niveau de la rédaction. C’est quand on a démontré l’absurde que l’on conclut. Et on a bien fait un raisonnement par implications pour y aboutir.
Ces deux assertions étant équivalentes, on n’écrit à aucun moment dans la preuve un énoncé faux, ce qui est structurellement d’un raisonnement par l’absurde
Vrai. Mais c’est l’équivalence logique avec $A\to B$ qui induit le fait que tu as fait une preuve en posant un énoncé faux.
En un sens, c’est comme si tu avais artificiellement coupé le morceau montrant l’équivalence $A\to B\iff B\to A$, qui lui fait appel à un raisonnement par l’absurde. Certes, le morceau restant ne fait plus appel à un énoncé faux, mais structurellement il y en a bien un qui a été employé.
Banni
La pirouette consistant à reformuler une preuve par l’absurde en une implication dont la conclusion est fausse me semble un peu artificielle.
Ce n’est pas du tout artificiel ! D’ailleurs l’exemple de la racine de 2 est pris ici pour parler de la différence entre une preuve de négation et une preuve par l’absurde (i.e. double négation).
Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte