Discussion:Modus ponens

Fusion entre Déduction logique et Modus ponens

Abandon (Jerome66 | causer 12 septembre 2006 à 07:07 (CEST)) :

Modus ponens est le nom latin et scientifique de la déduction logique (que tout le monde comprend) Les deux désignent la règle qui consiste à dire que Si A=>B et si j'ai A, alors, j'ai B. Camion 3 septembre 2006 à 10:51 (CEST)

Non. La déduction est une méthode qui permet de tirer des conclusions sur des faits donnés à partir d'autres faits. Un système de déduction logique est un ensemble de règles, en mathématique on parle aussi de "système de preuve" (cf. Méthode formelle (informatique)). Cela inclut le modus ponens en logique naturelle, mais on peut y ajouter comme c'est fait dans l'article la transitivité (A=>B et B=>C alors A=>C) ou encore le modus tollens. Cf. [1] ou plus technique [2] (pdf). knd 3 septembre 2006 à 13:15 (CEST)

"Modus ponens est le nom latin et scientifique de la déduction logique" faux: le modus ponens est un type de déduction entre autres (à côté de la règle de substitution par exemple). Il faudrait mentionner le modus ponens dans un article sur la déduction logique mais le modus ponens mérite néanmoins son propre article. D'ailleurs c'est ce que font wiki:de et wiki:en (et je pourrais citer encore une dizaine de liens interwiki) qui ont un article sur la déduction et un article sur le modus ponens. Apierrot 4 septembre 2006 à 12:56 (CEST)

rien à ajouter aux demos des précédents, donc laissons tomber la fusion. --Julianedm | ðΔ 6 septembre 2006 à 23:22 (CEST)

J'approuve totalement le propos d'Apierrot et la décision prise -Epsilon0 12 septembre 2006 à 19:32 (CEST)

Confusion

L'article ait une confusion entre la règle de modus ponens ou détachement, qui est une règle logique de l'implication, et la coupure qui est une règle sur les séquents (des déductions d'une certaines façon). Sans précautions, ça me semble catastrophique, et la conclusion (élimination du modus ponens, dans quel contexte !) n'a pas de sens. Proz (d) 28 novembre 2008 à 01:15 (CET)

J'avoue, c'est moi le fautif ... y a déjà plus de 2 ans (c'est pratique les historiques, d'ailleurs il est plus long que le texte)! Bon en effet, même si j'avais pris soin de préciser que le modus ponens concerne un système à la Hilbert et que la coupure concerne le calcul des séquents tu as tout à fait raison de préciser que l'un s'applique à des formules et l'autre à des déductions. Pour rattraper, je mets "déduction naturelle" (qui s'applique bien à des formules et non des déductions) au lieu de "calcul des séquents" et mentionne Prawitz, mais si tu vois comment améliorer encore plus sans tout supprimer vas-y ; càd que c'est sans doute pas très bien dit (mais pas d'autres idées pour améliorer) mais l'info est tout de même à signaler, non?--Epsilon0 ε₀ 28 novembre 2008 à 18:56 (CET)

Ma réaction était probablement exagérée. C'est tout à fait faux pour la déduction naturelle, donc c'était mieux avant (il ne faut pas que tu laisses cette version). L'élimination de la flèche est un modus ponens avec contexte, tu ne l'élimines pas. En calcul des séquents on peut voir la coupure comme une espèce de meta modus ponens, à l'image de ce qu'il y a sur en:. C'est plutôt une question d'expression : on avait l'impression en lisant rapidement que l'on pouvait éliminer le modus ponens dans un système à la Hilbert. Mettre bille en tête le calcul des séquents n'aide pas à comprendre à mon avis. Tu ne veux pas commencer par une explication "gentille", dire que ça s'appelle aussi détachement (nom assez parlant), parler de coupure bien plus tard (et écrire des implications, pas des non A ou B). Pourquoi il faut une règle par exemple. C'est quelque chose qui est souvent mal compris. Tu verras sur implication (logique) un énoncé qualifié de modus ponens ! Il y a un texte de Lewis Carroll sur le sujet il me semble (dans le style Achille et la tortue). Et parler éventuellement de coupure clairement dans le cadre de calcul des séquents dans une section à part. Proz (d) 28 novembre 2008 à 21:22 (CET)

Corrigé. Proz (d) 2 janvier 2009 à 15:13 (CET)

Demande d'explications

Le 7 février 2018 à 09:42 l'IP 145.242.20.58 a demandé d'expliquer pourquoi la tautologie [A ∧ (A ⇒ B)] ⇒ B n'est pas l'expression la plus exacte du modus ponens, même si on utilise l'opération implication matérielle p → q formellement définie par (¬p ∨ q) ). N. B. Il avait mis ça dans le texte de l'article, mais sa place est plus dans la page de discussion. --Pierre de Lyon (discuter) 7 février 2018 à 11:07 (CET)

J'aurais un premier commentaire, à savoir que le modus ponens, n'a pas à voir avec la proposition ¬p ∨ q. Autrement dit, p → q n'est pas défini par ¬p ∨ q. --Pierre de Lyon (discuter) 7 février 2018 à 11:11 (CET)

Il y a une explication, il faudrait savoir pourquoi elle ne convient pas à 145.242.20.58 (s'il l'a lue). Proz (discuter) 7 février 2018 à 12:55 (CET)

C'est aussi mon point de vue. --Pierre de Lyon (discuter) 7 février 2018 à 13:23 (CET)

Modus Ponens, Connecteur Implication et Relation de déduction

Bonjour,

J'ai lu plusieurs articles connexes à celui-ci en anglais et en français, et je suis assez perdu. Je pratique les mathématiques comme un étudiant, et donc je ne suis pas logicien. Je peux tout juste aspirer à enseigner un peu les maths.

J'espérais donc y voir un peu plus clair à l'aide de quelques articles Wikipédia, et ne pas avoir à m'enfiler plusieurs pavés de logique pour éclaircir les nuances entre connecteur implication, Modus Ponens et relation de déduction. Or là... j'ai du mal. J'espérais donc vous poser une ou deux questions afin d'éclairer ma propre lanterne et pour vous donner un retour sur l'effet que cela fait de lire les articles traitant sur le Modus Ponens et le connecteur implication.

Déjà, je vais essayer de reformuler ce que je comprends, en partant de l'usage courant que l'on fait de l'opérateur implication. Très couramment, un énoncé de mathématiques demande «Montrer que P⇒Q», et que (évidemment) le lecteur moyen comprend qu'il faut montrer que si P est vraie, alors Q est vraie par une relation de cause à effet. Mais j'ai l'impression que ce qu'il se passe dans les coulisses de «Montrer que P⇒Q» et que le lecteur moyen ne suspecte pas, est que le connecteur ⇒ étant une fonction logique, elle ne porte pas en elle intrinsèquement une quelconque relation de cause à effet entre P et Q attendue par le lecteur. Alors en quoi obtenons nous la relation de cause à effet attendue en démontrant que P⇒Q est vraie ? J'y ai réfléchi, et me dis que l'assertion P⇒Q étant vraie par défaut lorsque P est fausse, si l'on montre que lorsque P est vraie, Q est vraie par une relation de cause à effet, on montre en fait que quelle que soit la valeur de vérité de P, l'assertion P⇒Q est vraie. L'assertion P⇒Q est ainsi démontrée vraie quoi qu'il arrive, et donc P, P⇒Q ⊢ Q se réduit systématiquement à P⊢Q.

Mais l'essence de cette relation de cause à effet a lieu lors de la démonstration par le lecteur de l'énoncé «Montrer que P⇒Q» que si P est vrai, alors Q est vrai. Du coup en fait je suis perdu dans tous ces symboles et je me retrouve à penser qu'il est mieux d'écrire en français «montrer que si P alors Q». Car P⇒Q étant un connecteur pouvant être vrai même lorsque ses deux opérandes sont vraies sans avoir de lien de causalité, il ne renferme pas de relation de cause à effet, et P⊢Q étant (si je comprends bien) un symbole servant à formaliser un raisonnement, il n'exprime pas non plus l'éventualité que P puisse être vraie ou fausse, mais exprime que P étant vraie on déduit Q, au cours d'un raisonnement.

Ma seule vraie question dans tout ce laïus est: me suis-je trompé quelque part, ou c'était bien cela qu'il fallait comprendre (notamment ai-je bien saisi le sens du symbole ⊢ car j'ai un doute), et est ce que vous me donneriez raison pour dire que la seule formule exprimant correctement les liens de cause à effet est «Montrer que si P alors Q» en toutes lettres, et pas le symbole ⇒ ni le symbole ⊢?

Enfin, histoire de vraiment vous exposer à quel point je me fais des noeuds au cerveau, j'ai voulu me prouver à moi même que le connecteur ⇒ était assez indispensable pour exprimer un lien de cause à effet, car aucun autre connecteur ne permet de l'exprimer. Or ce fut un échec car je me suis souvenu que P⇒Q était équivalent à NON P OU Q, donc qu'en fait techniquement l'opérateur OU permettrait de définir le Modus Ponens par P, NON P OU Q ⊢ Q, ou on pourrait aussi utiliser le ET (qui peut d'ailleurs se définir à partir de OU et de NON par P ET Q = NON (NON P OU NON Q)), pour écrire P, NON (P ET NON Q) ⊢ Q comme définition du Modus Ponens.

Encore, ma question ici est: ai-je bien compris et est ce que ce que je viens de dire est vrai ?

Mes excuses encore pour la logorrhée, mais voici donc un retour d'étudiant en mathématiques qui a lu vos articles aussi studieusement que possible !

Merci beaucoup. — Le message qui précède, non signé, a été déposé par ByteMe666 (discuter), le le jour du printemps 2018

Bonjour  ByteMe666 : et avant tout bienvenue sur wikipédia.

Vos remarques m'interloquent car elles sont très pertinentes (/viennent d'un esprit qui clairement se pose de bonnnes questions) et montrent que les articles de wikipédia à eux seuls, en leurs diversité encyclopédiques, ne remplacent pas un cours structuré, comme peut en fournir un cours avec un prof ou un manuel (pour des conseils de manuels de logique suivant que vous êtes plutôt matheux ou philosophe je peux vous en conseiller sur ma page perso.) ou le projet qu'est la wikiversité

Sinon en 2 mots,

"p --> q" est une affirmation quelconque (du genre : "si 2=5, les fraises sont vertes") , disant " si p alors q"

"|- p --> q" qui est équivalent à "p |- q" (modulo le thm de déduction sur lequel nous n'avons pas d'article) , est l'affirmation (métalinguistique) que l'on a une preuve de "p --> q".

Bon en bref, il faut distinguer une affirmation quelconque, qui peut être vraie ou fausse de la forme "p-->q" de, ce qui est l'object de cet article , qui est une affirmation toujours valable en logique classique quelques soient les propositions, "p" et "q" impliquées : "p et p-->q permettent de déduire "q" par la règle du modus ponens.

J'espère avoir clarifié certaines de vos interrogations

--Epsilon0 (discuter) 20 mars 2018 à 21:21 (CET)

Bonjour  ByteMe666 : et bienvenue sur wikipédia. Je suis d'accord avec  Epsilon0 :, vous avez compris beaucoup de choses et vous vous posez les bonnes questions. Ce qui vous a peut-être embrouillé c'est de vous poser la question du raisonnement logique en termes de tables de vérité. Les tables de vérité ont des raisons historiques, mais elles sont un peu dépassées aujourd'hui en 2018 pour comprendre le raisonnement logique (je pourrai y revenir si vous le désirez). Compte tenu des questions que vous vous posez, vous auriez dû commencer par l'article Déduction naturelle (en nous aidant, au passage, à l'améliorer car il est peut-être encore un peu rude ). Le modus ponens y figure sous le nom d'élimination de la flèche. --Pierre de Lyon (discuter) 21 mars 2018 à 12:34 (CET)

Bonjour, Merci pour vos réponses. Je crois effectivement que la lecture de l'article sur la Déduction Naturelle est pas mal comme point de départ. Cela m'a conduit à enchainer sur l'article Calcul des Propositions. Je le lis actuellement, et je crois qu'en fait je mélange les notations de la Déduction Naturelle et celles des systèmes à la Hilbert. Le calcul des séquents en revanche ne me parle pas, mais je n'ai pas fait beaucoup d'efforts pour le comprendre. De toutes les notations que j'ai croisées et essayé de comprendre, le Modus Ponens exprimé par ⊢P ⊢P⇒Q (là une barre horizontale que je ne peux pas représenter) ⊢Q dans le paragraphe «systèmes à la Hilbert» me convient le mieux. La phrase «On remarquera que la règle d'élimination de l'implication est très proche du modus ponens, d'ailleurs on l'appelle aussi modus ponens» du paragraphe sur la Déduction Naturelle de l'article du Calcul des Propositions me renforce dans ce sentiment que ⊢P ⊢P⇒Q (barre horizontale) ⊢Q est le «vrai» modus ponens, bien que je crois comprendre que ces systèmes sont équivalents et qu'il n'y en a pas un plus vrai que l'autre, je veux juste dire que les notations sont plus satisfaisantes à mon esprit.

Je suis un peu gêné par l'ambivalence du symbole ⊢, qui semble signifier dans les systèmes à la Hilbert que ce qui se trouve à droite est vrai (comme dans la réponse de Epsilon0 au sujet de ⊢ p → q), et jamais rien n'est placé à gauche, alors que dans un système de déduction naturelle et dans beaucoup d'autres articles Wikipedia il signifie «je déduis», avec à gauche des prémisses et à droite la conclusion. L'article précise que le calcul des séquent emploie ⊢ de manière cohérente avec les systèmes à la Hilbert et la déduction naturelle, mais ne dit pas si le symbole ⊢ a au fond la même signification dans les systèmes à la Hilbert et la déduction naturelle.

C'est toujours un peu le fouillis dans mon esprit. Je voudrais juste poser une dernière question et m'arrêter là car je crois que pour comprendre d'avantage je dois faire un travail personnel et pas saturer cette page de discussion de l'article avec mes interrogations personnelles. Où puis-je trouver des commentaires ou explications ou informations générales, sur le lien remarquable qu'il semble y avoir entre la table de vérité du connecteur implication, le Modus Ponens, le Principe d'Explosion, et le Modus Tollens (contraposition) ? Je m'explique: P⇒Q est vrai lorsque P est vrai et Q est vrai, ce qui reflète le Modus Ponens; P⇒Q est vrai lorsque P est faux, ce qui reflète le principe d'explosion; NON (P⇒Q)= NON Q ⇒ NON P ce qui reflète le Modus Tollens (contraposition). Cet opérateur, qui en lui même ne renferme pas «l'essence» (je mets des guillemets, je m'exprime qualitativement) de la causalité entre opérandes et n'est qu'une fonction de vérité, semble pourtant bien refléter ces règles de déduction dans sa table de vérité.

Merci beaucoup et mes excuses encore pour la quantité de texte, peut-être faudrait-il déplacer cette discussion ailleurs, qui nourri de plus en plus mes réflexions personnelles que l'amélioration de l'article pour tous les lecteurs.

Salutations.--ByteMe666 (discuter) 21 mars 2018 à 17:37 (CET)

Calcul des séquents J'aurais envie de dire que le calcul des séquents est pour les spécialistes et qu'on peut différer son examen.

L'utilisation du symbole ⊢ dans les systèmes à la Hilbert est cohérente avec celle de la déduction naturelle, ⊢ P signifie de « de rien je déduis P », ce qui veut dire « P est un théorème », c'est la signification du symbole ⊢ dans les systèmes à la Hilbert.

Des explications sur le lien remarquable qu'il semble y avoir entre la table de vérité du connecteur implication et le reste, il faut les trouver dans l'article Logique intuitionniste qui explique qu'il n'y a hélas pas de lien remarquable. Le modus tollens en particulier n'est pas lié directement au modus ponens. Il faut revisiter nos conceptions et admettre une vision plus relativiste qui met la causalité de l'implication au centre des préoccupations.

Ne vous excusez pas, vos questions sont pertinentes et ne nous ennuient pas. --Pierre de Lyon (discuter) 21 mars 2018 à 19:03 (CET)

Bonjour, Je vais poursuivre cette conversation en correspondant avec vous sur votre page personnelle ou par un autre moyen. Je signale juste que je suis allé faire un tour sur la page de la Wikiversité, et c'était très prometteur ! Malheureusement beaucoup de pages sont incomplètes et je n'ai pas pu trouver les réponses que je voulais... Je songe moi même à faire une séquence de cours avec mon niveau de connaissances et une approche «langage parlé» pour captiver l'auditeur, mais sans pour autant complètement compromettre la rigueur. Je ne pense pas publier cela sur wikipedia (je pensais à Youtube) mais je serais heureux de partager ce que j'aurai fait si ce projet voit le jour.--ByteMe666 (discuter) 22 mars 2018 à 21:19 (CET)