Discuter:Déduction naturelle

Un article de Wikipédia, l'encyclopédie libre.

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)

[modifier] 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)

[modifier] 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)