Calcul des séquents
Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs de cet article est disponible ici.

En 1935 Gentzen a proposé la déduction naturelle, un formalisme pour décrire les preuves du calcul des prédicats, dont l'idée était de coller au plus près à la manière dont les mathématiciens raisonnent. Il a ensuite tenté d'utiliser la déduction naturelle (La déduction naturelle est une façon d'exposer les principes de la logique du premier ordre pour les rendre aussi proches que possible des façons...) pour produire une preuve syntaxique de la cohérence de l'arithmétique (L'arithmétique est une branche des mathématiques qui comprend la partie de la théorie des nombres qui utilise des méthodes de la géométrie algébrique et de la théorie des...), mais les difficultés techniques l'ont conduit à reformuler le formalisme en une version plus symétrique : le calcul des séquents. C'est dans ce cadre qu'il a démontré ce qui devait devenir l'un des théorèmes principaux de la théorie (Le mot théorie vient du mot grec theorein, qui signifie « contempler, observer, examiner ». Dans le langage courant, une théorie est une idée ou une connaissance spéculative, souvent basée sur l’observation ou...) de la démonstration : le théorème (Un théorème est une proposition qui peut être mathématiquement démontrée, c'est-à-dire une assertion qui peut être établie comme vraie au travers d'un raisonnement logique construit à partir d'axiomes. Un...) d'élimination des coupures. Dag Prawitz a montré en 1965 que ce théorème pouvait se transporter à la déduction naturelle

Définition (Une définition est un discours qui dit ce qu'est une chose ou ce que signifie un nom. D'où la division entre les définitions réelles et les définitions nominales.)

On donne ici une version légèrement modernisée par rapport à celle de Gentzen du calcul des séquents LK qui formalise la logique (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la fois raison, langage, et...) classique. On verra plus bas que sur le même principe on peut définir LJ, un calcul des séquents pour la logique intuitionniste, LL pour la logique linéaire... La définition ci-dessous suppose un minimum de familiarité avec le calcul des prédicats (Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage...).

Note terminologique

Le terme calcul des séquents est une traduction de l'anglais sequent calculus, lui-même hérité de l'allemand Sequenzenkalkül. La traduction littérale de l'allemand en français donnerait plutôt calcul des séquences et on trouve certains auteurs utilisant cette terminologie. Toutefois l'usage (L’usage est l'action de se servir de quelque chose.) le plus courant a imposé l'emploi du néologisme séquent.

Séquent

L'objet (De manière générale, le mot objet (du latin objectum, 1361) désigne une entité définie dans un espace à trois dimensions, qui a une fonction précise, et...) de base du calcul est le séquent, qui est un couple de listes finies (éventuellement vides) de formules. Les séquents sont usuellement notés :

A_1,\dots, A_n\vdash B_1,\dots, B_p

où les Ai sont les hypothèses et les Bj sont les conclusions du séquent. On voit ici apparaître l'innovation majeure du calcul des séquents : la symétrie parfaite entre hypothèses et conclusions. Un autre point (Graphie) important à noter est qu'une même formule peut apparaître plusieurs fois à gauche et/ou à droite dans un séquent, par exemple A1 peut être la même formule que An ; on dit alors que cette formule a plusieurs occurrences dans le séquent.

Interprétation d'un séquent

La notation séquent peut se comprendre comme une astuce syntaxique pour dénoter des formules particulières ; la virgule à gauche s'interprète comme une conjonction, la virgule à droite comme une disjonction et le symbole \vdash comme une implication, si bien que le séquent ci-dessus peut se comprendre comme une notation pour la formule :

A_1\and \dots\and A_n \rightarrow B_1\or \dots\or B_p

Règles

Les règles du calcul des séquents spécifient comment à partir d'un certain nombre (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».) (éventuellement nul) de séquents prémisses, on peut dériver un nouveau séquent conclusion. Dans chacune des règles les lettres grecques Gamma, Delta, etc. dénotent des suites de formules, on fait figurer les séquents prémisses au-dessus, séparés par un trait horizontal (Horizontal est une orientation parallèle à l'horizon, et perpendiculaire à la verticale. Une ligne horizontale va « de la gauche vers la...) du séquent conclusion. Elles se divisent en trois groupes : le groupe identité, le groupe structurel et le groupe logique.

groupe identité 
Image:LK_groupe_ident.png

Une discussion sur la règle de coupure figure plus bas. Remarquons que la règle axiome (Un axiome (du grec ancien αξιωμα/axioma, « considéré comme digne, convenable, évident en soi »)...) est la seule de tout (Le tout compris comme ensemble de ce qui existe est souvent interprété comme le monde ou l'univers.) le calcul qui n'a pas de séquent prémisse.

Pour les groupes structurel et logique, les règles viennent par paire (On dit qu'un ensemble E est une paire lorsqu'il est formé de deux éléments distincts a et b, et il s'écrit alors :) selon le côté, gauche ou droit, du séquent où elles agissent.

groupe structurel 
Image:LK_groupe_structurel.png

Dans les règles d'échange la notation σ(Γ) désigne une permutation (En mathématiques, la notion de permutation exprime l'idée de réarrangement d'objets discernables. Une permutation de n objets distincts rangés dans un certain...) des (occurrences de) formules figurant dans Γ. Les règles d'échanges sont responsables de la commutativité de la logique.

Les règles de contraction et d'affaiblissement expriment une forme d'idempotence des opérateurs "\scriptstyle \lor" et "\scriptstyle \land" de la logique  : une formule A est équivalente aux formules \scriptstyle A \lor A et \scriptstyle A \land A.

groupe logique 
Image:LK_groupe_logique.png

Les règles de quantificateurs sont soumises à des restrictions : dans les règles de \forall-droite et \exists-gauche, on demande que la variable (En mathématiques et en logique, une variable est représentée par un symbole. Elle est utilisée pour marquer un rôle dans une formule, un prédicat ou un algorithme. En...) x ne figure dans aucune des formules de Γ et Δ. La notation A[t / x] désigne la formule A dans laquelle la variable x est remplacée par un terme t.

Démonstrations

Une démonstration (En mathématiques, une démonstration permet d'établir une proposition à partir de propositions initiales, ou précédemment démontrées à partir de propositions initiales, en...) de LK est un arbre (Un arbre est une plante terrestre capable de se développer par elle-même en hauteur, en général au delà de sept mètres. Les...) de séquents construit au moyen des règles ci-dessus de façon à ce que chaque séquent soit conclusion d'exactement une règle ; la démonstration est terminée si l'on arrive à ce que toutes les feuilles de l'arbre soient des règles axiome. Le séquent racine de l'arbre est la conclusion de la démonstration. Voici un exemple de démonstration du principe de contraposition de l'implication ; pour simplifier on a omis les utilisations de règles d'échange et représenté en gras les (occurrences de) formules dans les séquents prémisses sur lesquelles porte chaque règle :

Image:LK_dem_contraposition.png

Discussion

Le calcul des séquents et les autres formalismes logiques

Le calcul des séquents, contrairement aux systèmes à la Hilbert ou à la déduction naturelle, n'est pas un formalisme très intuitif ; le propos de Gentzen était de résoudre certains problèmes techniques rencontrés en déduction naturelle lors de la démonstration de la cohérence de l'arithmétique. C'est pourquoi le calcul des séquents doit se penser comme un formalisme pour raisonner sur les preuves formelles plutôt que pour rédiger des preuves formelles, ce à quoi la déduction naturelle est plus adaptée. On peut toutefois facilement montrer que toute formule prouvable dans l'un des systèmes l'est également dans l'autre.

L'intérêt du calcul des séquents est de rendre explicite un grand nombre de propriétés de la logique :

  • la dualité hypothèse/conclusion exprimée par la symétrie parfaite entre la droite et la gauche dans les séquents ;
  • la symétrie de la logique classique exprimée par le partitionnement des règles en gauche et droite ;
  • les propriétés structurelles (commutativité, idempotence) exprimées par les règles du groupe structurel.

La règle de coupure

La règle de coupure est une généralisation (La généralisation est un procédé qui consiste à abstraire un ensemble de concepts ou d'objets en négligeant les détails de façon à ce qu'ils puissent être considérés de...) du modus-ponens. Pour le voir il faut considérer le cas particulier de la règle où :

  • Γ, Δ et Γ' sont des séquences vides de formules ;
  • Δ' contient une unique formule B.

Dans ce cas particulier les deux séquents prémisse de la règle deviennent respectivement \vdash A et A\vdash B tandis que le séquent conclusion devient \vdash B.

La règle de coupure joue (La joue est la partie du visage qui recouvre la cavité buccale, fermée par les mâchoires. On appelle aussi joue le muscle qui sert principalement à ouvrir et fermer la bouche et à mastiquer.) un rôle très particulier dans le calcul des séquents pour deux raisons :

  • elle est indispensable pour formaliser les preuves mathématiques ; en effet l'expérience montre que, à l'exception des démonstrations faciles de tautologies, la moindre preuve de mathématique utilise quasiment exclusivement la règle de coupure ;
  • plus techniquement, c'est la seule règle à violer la propriété de la sous-formule ; si on observe les règles du calcul des séquents on voit que pour chaque règle, sauf la coupure, les formules apparaissant dans les séquents prémisse sont encore présentes dans le séquent conclusion. Autrement dit, si une démonstration du calcul des séquents n'utilise pas la règle de coupure, alors toutes les formules apparaissant dedans sont des sous-formules du séquent conclusion, c’est-à-dire que le séquent conclusion de la démonstration est le plus compliqué de toute la démonstration.

La propriété de la sous-formule était très importante pour Gentzen car c'est elle qui permet de démontrer la cohérence du calcul : en effet le séquent le plus simple possible est le séquent vide qui ne contient aucune formule ni à gauche, ni à droite. Or ce séquent exprime une contradiction (Une contradiction existe lorsque deux affirmations, idées, ou actions s'excluent mutuellement.). Pour voir que le calcul est cohérent il suffit donc de voir que le séquent vide n'est pas prouvable ; mais une démonstration sans coupure du séquent vide ne devrait contenir que des séquents plus simples, et il n'y en a aucun. Donc toute démonstration du séquent vide doit utiliser la règle de coupure. Et voilà comment Gentzen a été conduit à démontrer son célèbre théorème d'élimination des coupures qui stipule (En botanique, les stipules sont des pièces foliaires, au nombre de deux, en forme de feuilles réduites située de part et d'autre du pétiole, à sa base, au point d'insertion...) justement que de toute démonstration d'un séquent, on peut extraire une démonstration sans coupure du même séquent, ce qui montre en corollaire (Un théorème est une proposition qui peut être mathématiquement démontrée, c'est-à-dire une assertion qui peut être établie comme vraie au travers d'un raisonnement logique construit à partir...) qu'il n'existe aucune démonstration du séquent vide. C'est en adaptant cette démonstration d'élimination des coupures au cas de l'arithmétique que Gentzen a produit sa preuve de cohérence de l'arithmétique.

Page générée en 0.180 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique