Discussion:Déduction naturelle

Discussion sur une potentielle suppression

moi j'ai pas le droit de proposer ton article à la suppression...

...mais on t'avait pourtant dit que tes théories perso n'avaient rien à faire ici :-(

ou alors bien camouflées ;-))) ... 82.224.88.52 14 fev 2005 à 20:45 (CET)

Mouais. Je dirais personnellement que je n'ai pas les connaissances nécessaires pour apprécier si l'article de Thierry Dugnolle est ou non un exposé de ses « théories personnelles ». As-tu ce bagage, cher Jacques 0vion, ou bien interviens-tu seulement pour essayer de faire fuir à toutes jambes un nouveau contributeur de qualité ? That is the question... Hégésippe | ±Θ± 14 fev 2005 à 21:01 (CET)

Mdr que ce soit toi qui parle de faire fuir ; ma compétence se limite à la forme et non au fond ; Thierry a tenu compte de mes remarques ; il a en effet retiré cette nuit du présent article la phrase suivante en reconnaissant son caractère personnel Jacques 0vion 15 fev 2005 à 08:59 (CET)

L’intuitionnisme a beaucoup d’importance aux yeux de nombreux 
logiciens. Pour ma part je ne doute pas de la valeur de leurs travaux
mais je ne les comprends pas bien et je préfère de très loin la
tolérance de la logique classique et des théories des ensembles au
purisme parfois sectaire des intuitionnistes.

On est très loin des théories personnelles que tu supposais. Caton 15 fev 2005 à 09:02 (CET)

Je trouve ce texte censé, bien écrit et intéressant. Manifestement, l'auteur maîtrise son sujet. On peut reprocher au texte d'être un peu long ; une fomulation plus formalisée l'aurait raccourci et rendu plus clair aux lecteurs habitués à lire des mathématiques formelles, mais j'imagine que l'auteur a eu en vue d'être lu surtout par des lecteurs "non initiés" et je ne l'en blâmerai pas. Cela dit, j'attends la suite avec curiosité. CD 14 fev 2005 à 21:53 (CET)

Et 82.etc. se moque du monde d'une manière assez grossière. Caton 14 fev 2005 à 22:00 (CET)

Mon inculture n'est pas aussi grossière la tienne quand tu avais cru bon rectifier la phrase suivante 82.224.88.52 14 fev 2005 à 22:23 (CET)

À cause du changement de calendrier, Sainte Thérèse d'Avila est morte dans le nuit du 4 au 15 octobre 1582.

Mais oui, 82, détourne donc mes propos. Il est maintenant clair pour moi que ton but est de nuire à cette encyclopédie. Caton 15 fev 2005 à 07:21 (CET)

mon but n'est pas de nuire à wikipédia même si je m'accorde des moments de trollage ici et là ; la plupart rigolent, quelques-uns râlent mais au moins je le fais de façon ouverte ; cela est loin d'être ton cas dans tes nombreux traficotages de dates tellement subtils qu'ils subsistent des semaines et doivent bien faire rigoler les détracteurs de notre wiki 82.224.88.52 15 fev 2005 à 10:12 (CET)

Explique-moi donc un peu mes nombreux traficotages. Je vois que ton but est de détourner l'attention vers moi par la calomnie, pour faire oublier le caractère incongru et injurieux de tes interventions. C'est un peu grossier comme truc. Caton 15 fev 2005 à 10:22 (CET)

C'est toi qui a commencé à m'injurier tout en trollant hors sujet sur cette page ; pourquoi as-tu refusé ce matin d'en débattre à l' endroit adéquat ; moi, je n'en veux à personne en particulier (Floreal me fait rigoler à chaque fois) et certainement pas à toi qui es nettement plus cultivé que la moyenne et dont j'ai juste souri en me disant que tu te trompais de bonne foi quand j'avais vu deux fois en janvier que tu étais faché avec les dates... alors... pourquoi ne pas admettre qu'il puisse m'arriver de me tromper moi aussi ??? 82.224.88.52 15 fev 2005 à 11:39 (CET)

Paragraphe d'accueil

J'attache une grane importance a ce chapeau. Il sert a cadrer l'exposé qui suit, mail il sert aussi au lecteur superficiel de l'encyclopédie (cela m'arrive souvent) de prendre une connaissance rapide de ce dont il est question. Ce chapeauci est presque parfait. Il manque pourtant selon moi une phrase pour dire comment la théorie a évolué depuis (pas une thèse, une phrase!)Ibn Harwa (d) 26 septembre 2012 à 23:04 (CEST)

Les règles de déduction pour les quatre opérateurs booléens fondamentaux

Je crois qu'il serait plus judicieux, vu le titre du paragraphe, d'organiser le dit paragraphe en quatre sous-paragraphes (et non six), à savoir un sous-paragraphe par opérateur, avec dans chaque paragraphe, la règle d'introduction et la règle d'élimination de l'opérateur. Cela rendrait l'article plus lisible. Theon 19 janvier 2006 à 09:58 (CET)

Arbres

Cet article était catastrophique et commence à ressembler à quelque chose de sérieux, merci Theon c'est du beau travail. Une suggestion toutefois, la notation des déductions comme suites de formules, avec ses règles un peu obscures de décalage pour noter les décharges d'hypothèses, étaient en vogue au milieu du siècle dernier mais est complétement obsolète aujourd'hui ; elle se justifie à l'extrême limite par des raisons de lisibilité (et encore c'est très discutable) mais n'a aucune propriété mathématique. On préfère de loin définir et noter les déductions comme des arbres. Pour décharger les hypothèses dans la flèche intro, on les barre ou on les met entre crochet :

                       [A]
                        .
                        .
                        .
                        B
                       ----
                       A->B

Ça n'est pas super propre car on ne voit pas le lien entre l'hypothèse déchargée et la règle responsable de cette décharge ; par contre ça a l'avantage de rendre quasiment évident l'isomorphisme de Curry-Howard avec le lambda-calcul typé. Le défaut peut se corriger en donnant un nom à chaque règle de flèche intro et en mentionnant ce nom au niveau des hypothèses déchargées (par exemple en les préfixant par le nom pour emprunter une notation du lambda-calcul typé :

                      [x:A]
                        .
                        .
                        .
                        B
                       ---x
                       A->B

De cette façon l'isomorphisme de CH est encore plus évident.

Je compte passer à cette définition/notation quand je trouverai le temps de m'y mettre.

Laurent de Marseille 2 février 2006 à 23:23 (CET)

Tout à fait d'accord, sauf que je garderais quand même quelquepart les preuves écrites dans ces notations, puisque,la notation est expliquée correctement, quelqu'un s'est fatigué à les saisir et elles ont un intérêt au moins historique. Après tout c'est l'usage d'une encyclopédie : on peut croiser ça dans un ouvrage, et vouloir des explications.

En "small" en fin d'article, avec en préambule les réserves que tu donnes ci-dessus ? Proz 3 mai 2006 à 13:08 (CEST)

Je suis le "quelqu'un" en question, mais je n'avais adopté cette notation en suites de formules que parce que le rédacteur initial avait adopté cette convention, et aussi, parce que la mise en forme était plus facile à faire dans l'encyclopédie que sous forme d'arbre. Il n'y a aucun inconvénient à la modifier. Par contre, il ne me paraît pas utile de garder les mêmes preuves dans deux notations différentes, ce qui alourdirait l'article (sauf éventuellement pour un unique exemple, placé dans un paragraphe traitant éventuellement des diverses conventions de notation possible, si on juge un tel paragraphe nécessaire). On trouve le même inconvénient par exemple dans les articles traitant de tel ou tel algorithme et où chacun y va de sa traduction dans son langage préféré ; il n'y a rien de plus exaspérant que de lire une suite de programmes identiques écrits dans des langages différents. Un seul suffit. Je pense qu'il en est de même ici. Theon 4 mai 2006 à 17:30 (CEST)

Je suis d'accord avec Laurent sur le choix de la notation. Si le texte actuel n'existait pas, je ne verrais vraiment aucune urgence à relater cette notation de Fitche (d'après l'article), que je vous remercie cependant de m'avoir fait connaître. Je comprends votre souci qui est pédagogique. Le mien était plus "encyclopédique". Le souci d'avoir une notation linéaire à peu près lisible peut se comprendre dans certains contextes. Si l'on garde quelquechose, il faut que ça reste clair (je dirais plutôt deux exemples biens choisis, un simple, un avec branchement). On pourrait donner une autre convention de notations en arbre (séquent), plus lourd mais qui lui a vraiment son intérêt pour les démonstration par induction sur la structure de la preuve style complétude (les changements de notation sont parfois utiles) mais ce n'est pas le plus urgent. Proz 4 mai 2006 à 21:18 (CEST)

Séquents naturels

Je fais des tests. Outs (d) 2 avril 2009 à 14:49 (CEST)

Oui, mais il est mieux que tu les fasses en te créant une sous page perso comme Utilisateur:Outs/Séquents naturels que je t'invite à bleuïr --Epsilon0 ε₀ 2 avril 2009 à 22:47 (CEST)

Ca marche. En fait j'aurais bien aimé avoir des avis sur le fait de présenter la déduction naturelle sous forme de séquents. Je suis d'accord que ce n'est pas la présentation classique, et qu'il n'est pas forcement souhaitable de multiplier les présentations légèrement différentes de la même chose (comme les sur les pages d'algo avec les 36 lang de prog). Mais de cette manière c'est vraiment plus didactique, quoique que légèrement plus verbeux pour les exemples. De plus si on pouvait aligner les formules cela serait plus compacte et lisible, j'ai essayé avec les tableaux WP mais ce n'est pas très concluant je trouve. Outs (d) 3 avril 2009 à 09:38 (CEST)

lien vers wikiversité

Faudrait-il faire un lien vers [1] ? Mais je ne sais pas comment le faire de manière propre, il y a un modèle qui existe je crois. Outs (d) 2 avril 2009 à 16:31 (CEST)

Mais j'avoue que je ne savais pas avant de tenter, l'url est : "http://fr.wikiversity.org/wiki/Fondements des mathématiques/La logique/Déduction naturelle" et le bandeau donne : {{wikiversité|Fondements des mathématiques/La logique/Déduction naturelle|Déduction naturelle}} . Sinon je ne sais trop quel est la qualité de cette page, j'ai parfois vu des trucs en logique sur wikiversité, qui, ben, m'ont fait fuir lâchement . --Epsilon0 ε₀ 2 avril 2009 à 22:43 (CEST)

hum j'ai l'impression que la page wikiversité est une copie de la page wikipedia version fevrier 2005. Mais l'article ici même a beaucoup changé depuis, alors qu'il a plutôt stagné là bas. Outs (d) 3 avril 2009 à 10:13 (CEST)

Il y a une origine commune. Je propose de supprimer ce lien (pour les mêmes raisons qui ont fait que cette page a évolué). Il existe une version plus proche, Style de Fitch pour la déduction naturelle, mais qui a été corrigée elle aussi. La wikiversité a repris (sans compétences particulières apparemment) les éléments d'un wikibook inachevé sur les fondements. Celui-ci est un travail philosophico-logique très personnel, pas du tout adapté à ce transfert, et très contestable par certains aspects (mais avec des choses justes). L'un des problèmes, c'est que le vocabulaire n'est pas standard (anhypothétique, séquence, ...). Proz (d) 4 avril 2009 à 16:07 (CEST)

Quoi, quoi pas standard ? "Les lois logiques sont des vérités anhypothétiques" c'est très bon ça dans une copie de philo, à mélanger avec du "hypothético-déductif" et l'inévitable "synthétique a priori" ;-) --Epsilon0 ε₀ 4 avril 2009 à 20:45 (CEST)

C'est fait, je l'ai mis en commentaire en fait. Désolé pour le dérangement :) Outs (d) 4 avril 2009 à 18:58 (CEST)

Ca me convient aussi et ça m'a appris la syntaxe d'un nouveau modèle. --Epsilon0 ε₀ 4 avril 2009 à 20:45 (CEST)

Problème de lisibilité

L'article manque de lisibilité en présentant des formules sans expliquer comment les lire. Par exemple après la première occurence de «A ∧ B» il faudrait écrire «(lire A et B)» et éventuellement pointé vers l'article détaillant le symbole. — Le message qui précède, non signé, a été déposé par Psychoslave  (discuter), le 30 juillet 2009 à 09:28

Je ne comprends pas bien ce que signifie « lire une formule ». On pourrait aussi bien vocaliser «A ∧ B» comme « A and B » ou « A avec B » ou « A chapeau-pointu B », en revanche on le lit «A ∧ B». Je crains que le concept de « lecture » n'apporte plus de confusion que de clarification. --Pierre de Lyon (d) 1 août 2009 à 23:28 (CEST)

Oui mais non, je confirme que préciser comment lire est indispensable ici. On a besoin de pouvoir rattacher les symboles à des sons et mieux encore à des concepts. Tel qu'il est l'article est un ramassis de symboles incompréhensibles, un peu comme si on empilait un suite de kanji pour un public francophone, qui ne saurait donc ni les prononcer et encore moins y voir un sens quelconque. --Psychoslave (d) 24 janvier 2011 à 10:21 (CET)

Il me semble que cette affirmation est excessive. Comme il s'agit de logique symbolique ou formelle, il me semble qu'un minimum d'utilisation de symboles est nécessaire. Autrement ce serait comme si on essayait d'évoquer l'écriture du japonais sans écrire aucun kanji. Quant à la lecture des symboles logiques, je ne connais aucun consensus et c'est peut-être mieux ainsi, car les symboles logiques n'ont pas comme but ultime d'être prononcés. --Pierre de Lyon (d) 25 janvier 2011 à 09:20 (CET)

Je n'ai jamais dit qu'il fallait retirer les symboles, mais qu'il fallait les introduire avec une prononciation. Comment lire un article sans le prononcer ? Est-ce que les articles mathématiques peuvent se permettre de déroger aux règles les plus élémentaires d'accessibilité ? --Psychoslave (d) 25 janvier 2011 à 18:18 (CET)

Pourquoi "à des sons et mieux encore à des concepts" ? Pourquoi "ni les prononcer et encore moins y voir un sens quelconque ? Et les sourds-muets, ils pensent comment ? Y a-t-il un (des) article(s) de WP qui parle des liens entre vocalisation, audition, et conceptualisation ? (et où cette discussion serait p.e. plus opportune) Anne Bauval (d) 25 janvier 2011 à 19:56 (CET)

Je ne sais pas pour ce qui est des sourds et muets, mais l'accessibilité c'est une démarche visant à rendre un contenu aussi universel que possible. Or moi là qui fait partie de cet univers, je trouve l'article peut accessible. Personnellement, j'ai besoin de pouvoir prononcer une phrase quand je la lit, particulièrement quand il s'agit d'un sujet que je ne maîtrise pas. Si ce que je vois n'est pas un mot, c'est un objet graphique que je peux essayer de transposer en mots avec plus ou moins de succès (un cercle bleu ayant une intersection avec un triangle jaune tous deux inscrits dans un carré vert, par exemple). --Psychoslave (d) 26 janvier 2011 à 10:41 (CET)

Rien n'empêche un individu qui a une mémoire et une compréhension auditive de prononcer les symboles dans sa tête, mais il ne doit pas imposer sa prononciation aux autres, surtout quand cette prononciation induit un concept faux. Il n'y a pas en logique de concept de « se lit » ou « se prononce ». --Pierre de Lyon (d) 27 janvier 2011 à 13:06 (CET)

D'abord les japonais qui lisent un Kanji le lisent à haute voix s'ils le veulent. Le Kanji fait référence à un langage parlé. Ensuite si l'on en vient à s'interroger sur les sourds muets, on peut se demander comment ils lisent un pièce de Racine, dont peu de gens pensent que la lecture est obligatoirement silencieuse. Je crois que pour la plupart de l'humanité un texte se lit à voix haute. Un texte logique comme un autre. Un anglais pourra lire "A and B" là où un français dira "A et B" mais l'un et l'autre lisent. A l'école on apprend à lire en prononçant. Pourquoi ne devrait on pas lire a voix haute les textes logiques, cela m'apparaît ahurissant. S'il n'y a pas consensus sur la façon de lire, c'est normal de le dire d'expliquer les points de vue habituels sur le sujet, c'est à dire de faire un travail d'encyclopédie. Il me semble, mais peut-être suis-je dans l'erreur, que tout le monde francophone lit et, ou, non, implique, logiquement équivalent de la même façon. Ne pas vouloir donner cette clé de lecture, c'est vouloir réserver wikipédia aux seuls initiés. Est-ce bien ce que nous voulons?Ibn Harwa (d) 24 septembre 2012 à 17:26 (CEST)

Évidemment que non, il suffit de lire la définition de L'article parfait pour trouver les deux points suivants :

• Il commence par une définition et une description claire du sujet. L'introduction amène et explique le sujet clairement et précisément, sans entrer dans des détails inutiles : c'est un résumé introductif.
• Il est compréhensible. Il est assez clair pour être facilement saisi, entre suffisamment dans les détails, explore avec soin le sujet, et est intelligible aussi bien par les néophytes que par les experts. --Psychoslave (d) 27 septembre 2012 à 10:08 (CEST)

Je vais donner un exemple précis de lecture qui est très mal à propos. En COQ, il existe des symboles syntaxiques < et > que l'on appelle en typographie des chevrons, mais que toute la communauté (le cercle des initiés) appelle des piquants. Comment doit-on suggérer de lire ces signes? Personnellement chaque fois que j'entends le mot « piquant », ça me gratte et me démange.

Question subsidiaire: Y a-il un consensus que la façon de lire le signe « $\vdash$ »?

1. thèse?
2. T couché ?
3. vdash ?
4. de ... on déduit ... ?
5. infère ?

Je suis sûr que j'en oublie.--Pierre de Lyon (d) 16 octobre 2012 à 19:03 (CEST)

La variable introduite avec l'universelle

J'espère ne pas mal utiliser la page de discussion, mais la règle d'introduction de $\forall$ précise que la variable x ne doit apparaître dans aucune des hypothèses non déchargées. Si j'ai bien suivi, dans cette règle, P n'est pas déchargée, et donc x n'apparaît pas dans P. Mais dériver $\forall$ x P quand P ne contient pas x n'a pas grand intérêt... Donc, soit j'ai raté quelque chose, soit il y a une erreur, soit c'est pas clair. Quelqu'un pourrait-il éclairer le sujet? Merci. — Le message qui précède, non signé, a été déposé par un utilisateur sous l’IP 81.67.23.175 (discuter), le 31 octobre 2010 à 13:16. Oups, j'ai oublié la signature...--81.67.23.175 (d) 31 octobre 2010 à 15:23 (CET)

Tu utilises correctement la page de discussion. Je vais essayer d'éclairer ce point. Dans une notation avec des séquents, en supposant que les hypothèses $h_{1},...,h_{n}$ non déchargées forment l'ensemble de clauses $\Gamma$, on écrit $\Gamma \vdash P$. Si $x$ n'apparait dans aucune des clauses $h_{1},...h_{n}$ (on ne dit rien à propos de $P$ qui peut contenir $x$ puisque ce n'est pas une hypothèse, on dit seulement que la démonstration de $P$ à partir de $\Gamma$ ne fait pas référence à $x$) alors on peut en déduire $\Gamma \vdash \forall xP$. On peut ainsi démontrer des propositions fort intéressantes. --Pierre de Lyon (d) 31 octobre 2010 à 15:34 (CET)

Restructuration

Je trouvais que l'article était trop compliqué dès le début et en même temps ne va pas assez loin.

A propos des règles etc.

Je me suis permis de ː

• Expliquer la déduction naturelle en gros dans la section "les principes de la déduction naturelle"
• Mettre les règles dans des tableaux dans la section "déduction naturelle en logique propositionnelle"
• Ajouter une section "Discussions" si le lecteur veut aller plus loin : logique du premier ordre (plus dur à cause des substitutions), logique intuitionniste, les différentes présentations, etc.

--Fschwarzentruber (discuter) 3 mai 2016 à 17:52 (CEST)

A propos du début de l'article

• J'ai supprimé la mention de la logique du premier ordre au début pour minimiser le nombre de concept dans le chapeau, mais aussi pour dire qu'il y a PLEIN de système de déduction naturelle pour d'autres logiques etc.
• J'ai revu qq phrases. Par exemple, l'article disait " pour représenter les preuves en logique du premier ordre de manière aussi proche que possible des façons naturelles de raisonner. ". Mais on a l'impression que c'est "les preuves en logique du premier ordre" de manière absolu. Alors que la notion de preuve dépend du système de déduction ! J'ai reformulé en "Les règles des démonstrations sont proches des façons naturelles de raisonner."

Tâches à réaliser pour l'article

Je pense qu'il faut maintenant :

• Ajouter un exemple simple au début (pt celui de la pluie, du sol glissant et sol mouillée mais c'est bizarre) et montrer une démonstration en déduction naturelle que tout le monde peut comprendre d'un coup
• Revoir l'historique. (S'inspirer de l'historique en anglais.. mentionner Lemmon etc., reformuler des phrases imprécises)
• Enrichir la section "Discussions". Parler ici de choses spécialisées. De logique du second ordre, de Curry-Howard, etc.

--Fschwarzentruber (discuter) 4 mai 2016 à 11:28 (CEST)

Introduction et élimination du faux

Il me semble qu'il y a une interversion de l'introduction et de l'élimination du faux. D'autre part, la règle de réduction à l'absurde n'est ni une introduction, ni une élimination et a un statut à part, comme cela est dit dans le texte, mais n'apparait pas dans le tableau. --Pierre de Lyon (discuter) 26 octobre 2016 à 22:04 (CEST)

J'ai éliminé cette incohérence. --Pierre de Lyon (discuter) 27 octobre 2016 à 17:55 (CEST)

Merci beaucoup. C'est beaucoup mieux comme cela.--Fschwarzentruber (discuter) 27 octobre 2016 à 18:24 (CEST)

Lien vers "Calcul des propositions"

La phrase "L'article calcul des propositions donne une variante de la déduction naturelle avec des séquents spécifiques, dit « naturels », où les hypothèses sont gardées comme un contexte et où les hypothèses n'ont pas à être déchargées, mais disparaissent du contexte." est bizarre.

• Pourquoi l'article Calcul des propositions présenterait des règles de déduction naturelle ? Elles devraient être dans cet article ǃ
• Ensuite, ça ne sert à rien de représenter toutes les règles avec des séquents dans une encyclopédie, si ?

Qu'en pensez-vous ? Que faire ? Supprimer cette phrase et supprimer les règles dans l'article calcul des propositions ? --Fschwarzentruber (discuter) 27 octobre 2016 à 18:22 (CEST)

Je suis d'accord qu'une variante de la déduction naturelle devrait apparaître dans cet article plutôt que l'article Calcul des propositions ; d'autant plus que cette variante est importante puisque c'est aujourd'hui l'une des façons standard (pour ne pas dire la manière standard) de présenter la déduction naturelle (cf. le David-Nour-Raffalli). Pour cette raison je ne suis pas d'accord que ça ne sert à rien de représenter toutes les règles avec des séquents.

--Laurent de Marseille (discuter) 28 octobre 2016 à 22:41 (CEST)

Bonjour Laurent. Je partage votre avis. Avec la présentation avec des séquents, la structure d'arbre fait que la structure d'arbre est visible. Les hypothèses déchargées sont claires car elles sont à gauche de |--. Le seul point négatif est qu'un tel arbre prend beaucoup de place ǃ La présentation avec les hypothèses déchargées (présentes dans l'article actuel) résout le problème de la place (les hypothèses ne sont écrites qu'une fois). La présentation "à la Fitch" est chouette aussi mais la structure d'arbre n'est plus visible et il faut numéroter les lignes pour montrer la structure d'une démonstration. Pt que le mieux serait de montrer toutes les présentations. Bonne journée. --Fschwarzentruber (discuter) 30 octobre 2016 à 13:56 (CET)

Justement les 3 présentations figurent dans la section Différentes présentations des règles et des démonstrations, ça me semble pas mal ainsi non ?

--Laurent de Marseille (discuter) 30 octobre 2016 à 17:51 (CET)

J'avais retapé un peu cette section à l'époque. C'est rudimentaire. C'est bien possible que cela suffise pour wikipedia. Sinon, l'article devient trop long et lourdingue. Maintenant donc ǃ ː) Que faire ?

• Supprimer brutalement le contenu correspondant aux règles de la déduction naturelle écrite en calcul des séquents dans l'article "Calcul des propositions" ?
• Remplacer les règles données dans cette article par les règles écrites avec des séquents (j'aime mais ça a le défaut d'être lourdingue car on écrit les hypothèses non déchargées plusieurs fois partout dans l'arbre) ? Franchement, Laurent, je te comprends.

Bonne soirée ǃ --Fschwarzentruber (discuter) 30 octobre 2016 à 20:16 (CET)

Je n'ai pas trop regardé l'article sur le calcul des propositions ; a priori je proposerais de... ne rien faire. Pas de raison de supprimer les règles du calcul des propositions, elles sont certes redondantes avec celles figurant ici mais ça ne sera pas la première redondance dans wp, et celle-là ne me semble pas trop grave. On peut même profiter de leur existence pour renvoyer dessus dans la section où l'on parle de présentation avec des séquents.

En tout cas je ne pense pas que ça soit nécessaire de remplacer les règles du présent article par celles avec des séquents ; c'est nécessaire dans un cours sur la DN quand on veut démontrer les théorèmes de normalisation par exemple, mais ici la présentation choisie est d'une part la présentation historique, d'autre part la présentation la plus simple, ça me semble donc approprié pour wp.

D'autres avis ?

--Laurent de Marseille (discuter) 31 octobre 2016 à 16:54 (CET)

Je crois que je suis responsable de la phrase incriminée, parce que j'avais constaté que cet article ne présentait pas la déduction naturelle avec des séquents alors que l'article calcul des propositions le faisait et je voulais signaler au lecteur curieux que cette autre présentation existait quelque part dans l'encyclopédie, sans commencer à dupliquer. Je suis d'accord Laurent de Marseille que la redondance ne nuit pas. --Pierre de Lyon (discuter) 1 novembre 2016 à 18:34 (CET)

Règle d'élimination quantificateur universel

Bonjour,

Ne manquerait-il pas une précondition pour l'application de cette règle?

Si on suppose $\forall xP$ avec $P:\exists y,y=x$ et que l'on substitue $P[y+1/x]$ on peut conclure: $P:\exists y,y=y+1$ ce qui ne semble pas acceptable. — Le message qui précède, non signé, a été déposé par 24.7.24.156 (discuter), le Le 29/04/2018 à 21h30

Bonjour, vous avez tout à fait raison, il manque la précision que je viens d'ajouter : où t est un terme et aucune occurrence libre de x dans P ne se trouve sous la portée d'un quantificateur liant une variable de t. Merci pour votre vigilance. Il faudrait d'ailleurs exemplifier la précision par votre contre exemple pour en montrer la nécessité. Je le fais quand j'ai plus de temps --Epsilon0 (discuter) 30 avril 2018 à 10:02 (CEST)

Merci à l'anonyme et merci à Epsilon0. Je me suis permis de modifier cette partie en utilisant la définition Def. 1.2.20 p. 22 du livre de David, Nour et Raffalli et les règles présentées p. 28-29. On permet l'application de la règle, mais c'est la définition de $P[y+1/x]$ qui est changé : on renomme les y liées pour avoir $\exists y',y'=y+1$. Si on ne renomme pas, on obtient effectivement $\exists y,y=y+1$ et cela s'appelle une capture de variables (cf. remarque 1 p. 22 de leur livre). Bonne journée et encore merci. --Fschwarzentruber (discuter) 30 avril 2018 à 12:46 (CEST)

Règles d'introduction et des règles d'élimination des connecteurs

Ici : https://fr.wikipedia.org/wiki/D%C3%A9duction_naturelle#D%C3%A9duction_naturelle_en_logique_propositionnelle

Manquerait-il le "∨" de disjonction dans la phrase : "Le tableau suivant donne les règles d'introduction et des règles d'élimination des connecteurs →, ∧ et ⊥." ?

--Lisanuna (discuter) 24 janvier 2020 à 11:47 (CET)

Bonjour, vous avez tout à fait raison, je viens de modifier. N'hésitez pas à faire de telles corrections vous même. --Epsilon0 ε₀ 24 janvier 2020 à 11:55 (CET)