Discussion:Calcul des séquents

Calcul de séquence/calcul des séquents

Le problème de doublon de cet article avec calcul de séquences est résolu. Une copie de la discussion autour de ce problème se trouve sur Discuter:Calcul de séquences.

Laurent de Marseille 7 février 2006 à 10:54 (CET)

Calcul des séquents et Calcul de séquences (fait)

Ces deux articles traitent de la même chose, le de:Sequenzenkalkül de Gerhard Gentzen. « Calcul des séquences » correspond à une traduction littérale de l'allemand, tandis que « calcul des séquents » utilise un mot inventé, vraisemblablement sous l'influence des traductions anglaises des travaux de Gentzen qui utilisent le terme « sequent » (en:sequent) pour éviter des confusions, du fait que le mot anglais « sequence » désigne déjà une suite (cette confusion est impossible en français). Le premier article est plus abouti que le deuxième, mais de nombreux liens pointent vers le deuxième, et il faudrait d'autre part expliquer cette double terminologie dans l'article fusionné... 83.177.240.162 18 janvier 2006 à 15:54 (CET)

Je suis responsable du doublon, j'ai créé l'article calcul des séquents. C'était peut-être une erreur mais l'article original, calcul de séquences ne me semblait pas réformable sans une réécriture complète (je m'explique sur ce point ci-dessous). J'ai d'ailleurs soumis préalablement la question dans Discuter:Logique mathématique mais je n'ai eu aucune réaction.

Il est inexact que beaucoup de liens pointent sur calcul de séquences, il y en avait 3 en provenance d'autres articles, dont 2 introduits par moi-même avant la création de calcul des séquents. Le 3ème provenait de l'article Gerhard Gentzen. J'ai modifié les 3 qui pointent désormais sur calcul des séquents.

Quant à la terminologie, je dois dire que j'ai découvert le terme calcul de séquences sur wikipedia, alors que je fréquente assidûment cette théorie depuis 20 ans. Je ne suis pas germaniste ; je veux bien croire que la traduction littérale du mot allemand est 'séquence', mais cela ne la rend correcte ni au sens mathématique, ni selon l'usage commun qui a toujours été à ma connaissance (et celles des quelques collègues à qui j'ai posé la question) d'employer le mot 'séquent'. Cela dit s'il s'avère que le terme est usité dans des sphères que j'ignore il faut évidemment le mentionner.

Sur le plan scientifique maintenant, j'ai dit que l'article calcul de séquences ne me semblait pas réformable, sans une réécriture complète. Tout d'abord sur le fond, cet article se concentre sur les aspects les plus formalistes et somme toute les plus mineurs du calcul des séquents en ommettant plusieurs points clefs : les raisons profondes ayant poussé Gentzen à introduire ce système, discussion de la règle la plus importante du calcul à savoir la règle de coupure, description du résultat fondamental. Sur la forme maintenant, l'article est rédigé dans un style très verbeux mais assez peu mathématique (il s'agit de logique mathématique). De plus il ignore les techniques modernes de présentation des systèmes formels.

Pour toutes ces raisons je pense que l'article calcul de séquences devrait disparaître dans la fusion proposée. Une autre possibilité, celle que j'avais en tête au départ, serait de laisser cet article dans la catégorie Logique et l'article calcul des séquents dans la catégorie Logique Mathématique.

J'ajoute pour finir que j'ai exactement le même type de réserves au sujet de l'article déduction naturelle, mais je ne recommettrai pas l'erreur de créer un doublon.

Laurent de Marseille 20 janvier 2006 à 23:55 (CET)

J'aurais envie de dire que Laurent a raison sur toute la ligne et j'appuie sans réserve ses propositions. Comme lui et sur une période un peu plus longue, je n'avais jamais entendu parlé de calcul des séquences. J'ai cependant l'avantage sur lui d'avoir lu Gentzen dans le texte ayant découvert que ses articles sont accessibles sur Internet. Le nom séquent ne me choque absolument, et du coup je parle sans vergogne d'antécédent et de conséquent.

(-: A vouloir tout mettre au féminin, «conséquent» donnerait quelque chose d'étrange.

Pierre de Lyon 21 janvier 2006 à 17:47 (CET)

En l'absence de réactions négatives je vais remplacer l'article Calcul de séquences par un redirect sur Calcul des séquents dans un avenir assez bref. Il n'y a pas de problème de fusion d'historique dans la mesure où je ne reprendrai rien de l'article Calcul de séquences.

Laurent de Marseille 28 janvier 2006 à 19:19 (CET)

Toujours aucune réaction négative. C'est fait.

Laurent de Marseille 7 février 2006 à 09:55 (CET)

Il est préférable, lorsqu'un article est transformé en redirect, de faire de même avec sa page de discussion, et de garder les discussions utiles près de l'article-cible. Solveig 7 février 2006 à 18:37 (CET)

Ah bon d'accord. Je n'ai pas trouvé d'explications très détaillées sur la conduite à tenir dans ce genre de circonstances alors j'ai un peu improvisé. Merci du coup de main.

Laurent de Marseille 7 février 2006 à 20:58 (CET)

Merci. Je précise que quand j'ai proposé la fusion je n'avais aucune connaissance du sujet (c'est d'ailleurs pour cela que je consultais la page), c'est pourquoi j'étais incapable de trancher moi-même en faveur d'une des deux terminologies. J'avais en fait déduit de la coexistence des pages que les deux étaient utilisées concurremment. L'explication que j'ai donnée à la double terminologie venait en fait de ce que j'avais lu sur wikipedia en anglais. Le « nombreux » était sans doute exagéré (en fait ça voulait dire plusieurs), mais le fait est que je m'étais retrouvé sur la mauvaise page plusieurs fois. 129.199.97.129 31 mars 2006 à 13:35 (CEST)

Les références

Il faudrait mettre un peu d'ordre dans les références. Pierre de Lyon (d) 7 mars 2009 à 10:27 (CET)

C'est fait. J'ai séparé la partie I (déd nat) de la II (sequent), c'était bien ça ? Je ne parle pas allemand mais ça a l'air d'être ça.

Sinon on peut enlever la section «Voir aussi» je pense, vu que les article sont en accès libre sur le site de Springer apparemment.

Outs (d) 12 mars 2009 à 19:12 (CET)

groupe logique

Y'aurait pas des erreurs sur le "et droite", "ou gauche" et le "implique gauche" ? Je pense qu'il faudrait renommer le gamma et le delta de la deuxième prémisse pour une autre variable. Comme dans la version en Outs (d) 8 mars 2009 à 22:10 (CET)

Il n'y a pas d'erreur : il est vrai qu'il existe d'autres formulations des règles, dans lesquelles les contextes des deux prémisses (le Gamma et Delta) sont différents mais on peut facilement montrer que les deux formulations des règles sont équivalentes. À noter que cette équivalence n'est vraie qu'en présence des règles structurelles (affaiblissement, contraction). En Logique Linéaire les deux formulations ne sont plus du tout équivalentes et définissent des connecteurs différents.

Le choix de cette formulation des règles binaires, dite formulation additive est motivé par le fait qu'elle est compatible avec logique intuitionniste, ce qui ne serait pas le cas d'une formulation multiplicative (avec des contexte différents dans chaque prémisse).

Laurent de Marseille (d) 8 mars 2009 à 22:41 (CET)

Merci pour l'explication :) Ce genre de considérations mériterai un petit paragraphe dans l'article AMA Outs (d) 12 mars 2009 à 19:14 (CET)

Indispensable?

Dans la section "La règle de coupure" il est écrit, à quelques lignes d'intervalle, à propos de la règle de coupure:

• elle est indispensable...
• ... la règle de coupure n'est jamais indispensable

N'y aurait-il pas un certain problème logique dans cette conjonction?

Taxipom (discuter)

En effet la formulation est maladroite. La règle de coupure est nécessaire au point de vue pragmatique, si l'on veut une démonstration courte. En revanche, pour toute démonstration d'une proposition il existe une démonstration sans coupure de la même proposition. Donc, au point de vue logique, on peut se passer de la coupure. --Pierre de Lyon (discuter) 21 avril 2014 à 18:16 (CEST)

Subjectif?

Bonjour,

«Le calcul des séquents, contrairement aux systèmes à la Hilbert ou à la déduction naturelle, n'est pas un formalisme très intuitif». C'est très subjectif, non? La construction du système à la Hilbert ne communique pas beaucoup de sens intuitif, contrairement au calcul des séquents. Cependant, plus loin l'article va dire que ce calcul est moins adapté à rédiger des preuves. Peut-être, il faut spécifier mieux ce que l'auteur a voulu sous-entendre dans la première phrase?.. - 89.110.28.135 (discuter) 3 juillet 2014 à 18:21 (CEST)

Je suis d'accord avec vous sur la subjectivité de cette affirmation. --Pierre de Lyon (discuter) 14 juillet 2014 à 20:09 (CEST)