Discussion:Principe d'explosion

Pour l'exemple intuitif

On pourrait mettre celui très célèbre de Russell déjà exposé sur wp ici.

Bon ce n'est qu'une suggestion avec caution historique, sur ce qui relève plus d'une blague improvisée par un prof en cours que d'une démonstration rigoureuse.

Il me semble que nous devons produire mieux en terme d'exemple compréhensible pour le lecteur, mais aussi, pour "anecdote", car célébrissime, mentionner que "si 0=1 alors Russell est le pape". --Epsilon0 ε₀ 15 janvier 2014 à 22:41 (CET)

Fais toi plaisir, il faut juste signaler que l’argument est plus rhétorique que logique, l'item 5 de la démonstration étant intéressant mais évidemment pas du tout de nature mathématique ;). Sur la compréhensibilité de l’exemple, tu penses que c'est trop formel, pas assez compréhensible ? On peut détailler l’étape 3 du raisonnement dans l’exemple, c'est le plus complexe, mais ça ne fait que ralonger l’exemple. Je sais pas trop comment faire plus concis. — TomT0m ^[bla] 16 janvier 2014 à 12:51 (CET)

J'ai un peu modifié l'exemple initial. C'est clairement améliorable, mais l'enchainement des étapes que tu avais mis me convient.

Pour la "pirouette" de Russell, que j'ai un peu hâtivement évoquée, ce sera sans doute à mentionner à terme en guise d'anecdote historique, mais songeons plutôt, pour l'instant à améliorer le fond du sujet :

* Traquer les encore erreurs de syntaxes et d'orthographes issues de la traduction + des points plus soutenus en vocabulaire technique ("proposition" != "énoncé", etc)

* lien précis vers les règles utilisées

* p.-e. développer sur la para-constance en l'absence actuelle d'un article comme en:Paraconsistent logic --Epsilon0 ε₀ 16 janvier 2014 à 21:36 (CET)

Origine du nom

Je n'ai jamais entendu parlé de ce concept de principe d'explosion. Je souhaiterais une référence et un historique. --Pierre de Lyon (discuter) 17 avril 2016 à 18:45 (CEST)

C'est très connu pourtant, "ex falso sequitur quod libet" renvoie des tas de résultats. C'est un principe contenu dans la logique classique (avant le XXème donc). j'avoue que je je maîtrise pas l'histo mais en feuilletant une ref on peut lire "since Aristotle, the Principle of Pseudo-Scotus (PPS), also knownsince medieval times as ex contradictione sequitur quodlibet (and also called thePrinciple of Explosion by some contemporary logicians) ..." donc c'est connu depuis la grèce antique on dirait. En tout cas il a son site Internet http://exfalsoquodlibet.com/ et son strip xkcd : http://xkcd.com/704/ . — TomT0m ^[bla] 17 avril 2016 à 19:17 (CEST)

Je me suis mal fait comprendre. Bien sûr, depuis que je fais de la logique, je connais « ex falso sequitur quodlibet ». Ce dont je n'ai jamais entendu parler c'est de l'expression « principe d'explosion ». Autrement dit nommer l'article « ex falso sequitur quodlibet » ne m'aurait pas surpris. En revanche, c'est son appellation « principe d'explosion » qui me surprend. De plus, si l'expression « principe d'explosion » est utilisée dans l'article, je demande à ce qu'elle soit sourcée. Qui l'a employée le premier? Quel livre l'utilise? . --Pierre de Lyon (discuter) 18 avril 2016 à 10:19 (CEST)

Ah pardon, bah c'est couramment utilisé en anglais (principle of explosion). C'est tout ce que je sais, sinon qu'en cherchant le terme en français dans google on en trouve des occurences assez facilement, par exemple https://books.google.fr/books?id=_rKMpQomnSYC&pg=PA96&lpg=PA96&dq=%22principe+d%27explosion%22&source=bl&ots=DdrI1K4y5N&sig=r86y6SaYiTMRriayhpfUpGsd99A&hl=fr&sa=X&ved=0ahUKEwick6_N3ZjMAhVLcD4KHaUyBo4Q6AEISjAK#v=onepage&q=%22principe%20d%27explosion%22&f=false ou sur scholar https://scholar.google.fr/scholar?start=10&q=%22principe+d%27explosion%22+logique&hl=fr&as_sdt=0,5 À titre de comparaison, la requête google scholar avec ta formulation : https://scholar.google.fr/scholar?start=20&q=%22ex+falso+sequitur+quodlibet%22+logique&hl=fr&as_sdt=0,5 (j'ai enlevé les résultats avec "logic" pour enlever les documents en anglais. C'est comparable en terme de nombre de résultat. — TomT0m ^[bla] 18 avril 2016 à 19:48 (CEST)

et sans le sequitur, guère de différence : https://scholar.google.fr/scholar?q=%22ex+falso+quodlibet%22+logique&btnG=&hl=fr&as_sdt=0%2C5

Je crois que je n’ai moi non plus jamais entendu « principe d’explosion ». Ce n’est pas parce que la locution « explosion principle » existe (= est employée) en anglais que sa traduction mot-à-mot existe en français. — Maëlan, le 8 novembre 2021 à 18:18 (CET)

Illustration du principe

Il est dit dans l’introduction que ex falso quodlibet existe en logique intuitionniste (ce qui est exact), mais l'illustration du principe est faite en logique classique.

En effet, en logique intuitionniste, $A\vee B$ signifie que ou bien j'ai une démonstration de $A$ ou bien j'ai une démonstration de $B$ ; c'est ce qui le différencie du $\vee$ classique. Puisque l'existence de citrons verts me dit que je n'ai pas de démonstration du fait que les citrons sont jaunes, alors j'ai une démonstration que le Père Noël existe. Puisque je n'ai pas menti en disant les citrons sont jaunes $\vee$ Père Noël existe, il ne me reste plus qu'à fournir cette démonstration de l'existence du Père Noël, que j'avais affirmé avoir sous la main. Pour cela, je vous donne rendez-vous en Laponie.

En gros, ce que je veux dire, c'est qu'en logique intuitionniste, ex falso quodlibet n'est pas si étrange que cela et que l'exemple devrait être reformulé, pour en tenir compte. En particulier, il ne faut pas parler d'« affirmations », mais de « démonstrations » ou de « preuves » comme disent certains. Pierre Lescanne (discuter) 25 juillet 2023 à 19:23 (CEST)
P. S. Les Québecois et les Sénégalais appellent « lime » ce que nous, Français, appelons « citrons verts », donc ils n'ont pas de démonstration que le Père Noël existe, de même qu'ils n'ont pas de démonstration qu'il existe des citrons verts !

J'ajoute que le paragraphe qui « présente » l'exemple commence par « Ces affirmations peuvent être, dans des conditions données, soit vraies, soit fausses » ce qui est le principe du tiers exclus. Donc un exemple qui se restreint à la logique classique n'est pas adéquat, alors qu'on vient de dire que le principe d'explosion est valable dans la logique intuitionniste. Je prose donc de supprimer cet exemple. --Pierre Lescanne (discuter) 12 août 2023 à 17:45 (CEST)

Comme il n'y a pas eu d'objection, j'ai supprimé le paragraphe.--Pierre Lescanne (discuter) 10 septembre 2023 à 09:59 (CEST)

Théorie de la démonstration

Les soi-disant démonstrations formelles du ex falso quodlibet sont toutes en logique classique, elles prétendent être formalisées en déduction naturelle, mais utilisent toutes artificiellement une règle exogène (résolution, élimination de la double négation, la troisième appelle d'ailleurs à tort reduction par l'absurde une introduction de la négation), n'utilisent pas le bon vocabulaire dans ce contexte ('théorème de la déduction' pour 'introduction de l'implication"). En fait le ex falso quodlibet correspond à une règle élémentaire de la déduction naturelle, qui est par ailleurs un cas particulier de la règle de réduction par l'absurde, elle même règle élémentaire de la déduction naturelle classique. Ces "démonstrations" ne font qu'obscurcir ce fait très simple, et ne justifient rien en réalité. Il est très improbable qu'on trouve des sources. Je propose de les effacer. Maintenant il faudrait parler correctement de la déduction naturelle, voire du calcul des séquents, de logique intuitionniste... Proz (discuter) 22 juillet 2024 à 18:14 (CEST)

Je suis pour supprimer cette partie, de manière générale il n'y a rien de très intéressant à essayer de donner une "démonstration" de l'admissibilité de cette règle en utilisant des règles ad hoc et plus complexe comme la règle de résolution. Et quant bien même on voudrait la garder, ça n'a rien à faire dans une section "Discussion" qui prétend donner un "argument en faveur du principe d'explosion" en se basant sur un système qui est basé dessus, alors que l'argument sémantique est convaincant. JeanCASPAR (discuter) 22 juillet 2024 à 20:58 (CEST)

Citrons verts

Je suis aussi d'accord pour la suppression de cette partie. Plus généralement, je ne suis pas favorable à mettre des démonstrations dans Wikipédia. De plus, je suis aussi opposé à l'insertion de phrases de la langue naturelle, du genre « tous les citrons sont jaunes », dans des démonstrations formelles. On est rarement loin du syllogisme. --Pierre Lescanne (discuter) 23 juillet 2024 à 16:43 (CEST)

Fait, il n'y avait déjà plus de citrons dans l'article par ailleurs. Il y aurait des choses à dire mais avec source, sinon on risque de retomber dans les dérives précédentes. Par exemple en logique minimale, si on démontre ⊥ à partir d'hypothèses qui n'utilisent ni ⊥ ni négation, alors n'importe quelle proposition est démontrable (par substitution).

Par ailleurs l'article parle de "élimination du faux", comme si c'était quelque chose de différent, mais je ne vois pas ce que ça peut être d'autre que le ex falso quodlibet (enfin une formalisation). Proz (discuter) 23 juillet 2024 à 18:31 (CEST)

Ah oui, c'est moi qui l'ai modifié, ça se mord effectivement un peu la queue. JeanCASPAR (discuter) 23 juillet 2024 à 18:48 (CEST)