Calcul des séquents

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

En logique mathématique et plus précisément en théorie de la démonstration, le calcul des séquents est un système de déduction créé par Gerhard Gentzen[1],[2].

Le nom de ce formalisme fait référence à un style particulier de déduction ; le système original a été adapté à diverses logiques, telles que la logique classique, la logique intuitionniste et la logique linéaire.

Un séquent est une suite d'hypothèses suivie d'une suite de conclusions, les deux suites étant usuellement séparées par le symbole \vdash (taquet droit[3]) ou \rightarrow dans l'œuvre originale de Gentzen. Un séquent représente une étape d'une démonstration, le calcul des séquents explicitant les opérations possibles sur ce séquent en vue d'obtenir une démonstration complète et correcte.

Historique et motivation[modifier | modifier le code]

En 1934[4] 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 pour produire une preuve syntaxique de la cohérence de l'arithmétique, 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 de la démonstration : le théorème d'élimination des coupures. Dag Prawitz a montré en 1965 que ce théorème pouvait se transporter à la déduction naturelle.

Définition[modifier | modifier le code]

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 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.

Note terminologique[modifier | modifier le code]

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 le plus courant a imposé l'emploi du néologisme séquent.

Séquent[modifier | modifier le code]

L'objet 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 A_i sont les hypothèses et les B_j 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 important à noter est qu'une même formule peut apparaître plusieurs fois à gauche et/ou à droite dans un séquent, par exemple A_1 peut être la même formule que A_n ; on dit alors que cette formule a plusieurs occurrences dans le séquent.

Interprétation d'un séquent[modifier | modifier le code]

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)

et signifie intuitivement :

A_1\text{ et } \dots \text{ et }  A_n \text{ impliquent }  B_1 \text{ ou }  \dots \text{ ou } B_p

mais le sens précis de ces symboles n'est donné que par les règles formelles (axiomes) qui suivent.

Lorsque la liste d'hypothèses est vide on peut l'interpréter comme le vrai (c'est-à-dire l'élément neutre de la conjonction) et lorsque la liste de conclusions est vide on peut l'interpréter comme le faux (c'est-à-dire l'élément neutre de la disjonction).

Règles[modifier | modifier le code]

Les règles sont de la forme : 
 \cfrac{\textrm{premisses}}
       {\textrm{conclusion}} \quad \textrm{nom}

Les règles du calcul des séquents spécifient comment à partir d'un certain nombre (é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 du séquent conclusion. Elles se divisent en trois groupes : le groupe identité, le groupe structurel et le groupe logique.

Groupe identité[modifier | modifier le code]

 \cfrac{\qquad }{ A \vdash A} \quad \textrm{axiome}

\qquad

\cfrac{\Gamma \vdash A, \Delta \qquad \Gamma', A \vdash \Delta'} {\Gamma, \Gamma' \vdash \Delta, \Delta'} \quad \textrm{coupure}

Une discussion sur la règle de coupure figure plus bas. Remarquons que la règle axiome est la seule de tout le calcul qui n'a pas de séquent.

Pour les groupes structurel et logique, les règles viennent par paire selon le côté, gauche ou droit, du séquent où elles agissent.

Groupe structurel[modifier | modifier le code]


\cfrac
{\Gamma \vdash \Delta}
{ \Gamma,A \vdash \Delta} 
\quad \mathrm{affaiblissement\ gauche}

\qquad

\cfrac
{\Gamma \vdash \Delta}
{\Gamma \vdash A,\Delta } 
\quad \mathrm{affaiblissement\ droite}


\cfrac
{\Gamma,A,A \vdash \Delta}
{ \Gamma,A \vdash \Delta} 
\quad \mathrm{contraction\ gauche}

\qquad

\cfrac
{\Gamma \vdash A,A,\Delta}
{\Gamma \vdash A,\Delta} 
\quad \mathrm{contraction\ droite}


\cfrac
{\Gamma \vdash \Delta}
{ \sigma(\Gamma) \vdash \Delta} 
\quad \mathrm{\acute echange\ gauche}

\qquad

\cfrac
{\Gamma \vdash \Delta}
{\Gamma \vdash \sigma(\Delta)} 
\quad \mathrm{\acute echange\ droite}


Dans les règles d'échange la notation \sigma(\Gamma) désigne une permutation des (occurrences de) formules figurant dans \Gamma. Les règles d'échanges sont responsables de la commutativité de la logique. Par exemple avec \Gamma = A_1, A_2 on aura \sigma(\Gamma) = A_2, A_1.

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[modifier | modifier le code]


\cfrac
{\Gamma \vdash A,\Delta}
{ \Gamma,\lnot A \vdash \Delta} 
\quad \lnot\mathrm{ gauche}

\qquad

\cfrac
{\Gamma,A \vdash \Delta}
{\Gamma \vdash \lnot A, \Delta } 
\quad \lnot\mathrm{ droite}


\cfrac
{\Gamma,A,B \vdash \Delta}
{ \Gamma,A\land B \vdash \Delta} 
\quad \land\mathrm{ gauche}

\qquad

\cfrac
{\Gamma \vdash A,\Delta    \quad    \Gamma \vdash B,\Delta}
{\Gamma \vdash A\land B,\Delta } 
\quad \land\mathrm{ droite}


\cfrac
{\Gamma,A \vdash \Delta    \quad     \Gamma,B \vdash \Delta}
{ \Gamma,A\lor B \vdash \Delta} 
\quad \lor\mathrm{ gauche}

\qquad

\cfrac
{\Gamma \vdash A,B,\Delta}
{\Gamma \vdash A\lor B,\Delta } 
\quad \lor\mathrm{ droite}


\cfrac
{\Gamma \vdash A,\Delta    \quad    \Gamma,B \vdash \Delta}
{ \Gamma,A\to B \vdash \Delta} 
\quad \to\mathrm{ gauche}

\qquad

\cfrac
{\Gamma,A \vdash B,\Delta}
{\Gamma \vdash A\to B,\Delta } 
\quad \to\mathrm{ droite}


\cfrac
{\Gamma,A[t/x] \vdash \Delta}
{ \Gamma,\forall x\cdot A \vdash \Delta} 
\quad \forall\mathrm{ gauche}

\qquad

\cfrac
{\Gamma \vdash A,\Delta}
{\Gamma \vdash \forall x\cdot A,\Delta } 
\quad \forall\mathrm{ droite}


\cfrac
{\Gamma,A \vdash \Delta}
{ \Gamma,\exists x\cdot A \vdash \Delta} 
\quad \exists\mathrm{ gauche}

\qquad

\cfrac
{\Gamma \vdash A[t/x],\Delta}
{\Gamma \vdash \exists x\cdot A,\Delta } 
\quad \exists\mathrm{ droite}


Les règles de quantificateurs sont soumises à des restrictions : dans les règles de \forall-droite et \exists-gauche, on demande que la variable x n'ait pas d'occurrence libre dans une des formules de \Gamma et \Delta.

La notation A[t/x] désigne la formule A dans laquelle la variable x est remplacée par un terme t, toutefois ce remplacement doit être sain : A ne doit pas contenir de sous-formule \forall y.B ou \exists y.By serait une variable libre de B apparaissant dans le terme t. Par exemple [y/x] n'est pas une substitution saine dans \forall z\exists y.P(x,y,z) car après remplacement de x par y on obtient : \forall z\exists y.P(y,y,z), une variable (ici y) du terme remplaçant x s'est fait capturer par le quantificateur \exists y.

Démonstrations[modifier | modifier le code]

Une démonstration de LK est un arbre 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 :

LK dem contraposition.png

Théorème d'élimination des coupures[modifier | modifier le code]

Aussi connu sous le nom de « théorème de Gentzen » ou « Hauptsatz » (parce que c'était le théorème principal des deux articles fondateurs de Gentzen), ce théorème énonce que toute démonstration en calcul des séquents peut être transformée en une démonstration de même conclusion, mais qui n'utilise pas la règle de la coupure.

La démonstration de Gentzen fournit un algorithme qui, appliqué à une démonstration quelconque, aboutit à une démonstration sans coupures du même séquent conclusion.

Helena Rasiowa (en) et Roman Sikorski (en) ont publié en 1959 une preuve sémantique du théorème de Gentzen pour le cas classique, qui montre l'existence de la démonstration sans coupures, mais ne donne pas un procédé (de normalisation) qui y conduit étape par étape.

Discussion[modifier | modifier le code]

Le calcul des séquents et les autres formalismes logiques[modifier | modifier le code]

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[modifier | modifier le code]

La règle de coupure est une généralisation du modus-ponens. Pour le voir il faut considérer le cas particulier de la règle où :

  • \Gamma, \Delta et \Gamma' sont des séquences vides de formules ;
  • \Delta' contient une unique formule B.

Dans ce cas particulier les deux séquents prémisses 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 un rôle très particulier dans le calcul des séquents pour deux raisons :

  • elle est presqu'incontournable pour formaliser les démonstrations mathématiques ; en effet l'expérience montre que, à l'exception des démonstrations faciles de tautologies, la moindre démonstration de mathématique utilise très souvent 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 qu'elle contient 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. On peut en effet montrer que si le calcul mène à une contradiction, c'est-à-dire si l'on peut aussi bien prouver \vdash A que \vdash \neg A, alors on peut, moyennant la règle de coupure, prouver le séquent vide \vdash : il suffit d'utiliser la règle de négation


\cfrac
{\vdash \neg A}
{ \neg \neg A \vdash }

puis la coupure


\cfrac
{\vdash \neg \neg A    \quad   \neg \neg A \vdash }
{ \vdash }

Ainsi, toute contradiction mène au séquent vide. On en déduit, par simple contraposition, que si le séquent vide n'est pas prouvable, c'est qu'il n'y a pas de contradiction.

Par ailleurs, il est évident que le séquent vide n'a pas de sous-formule... précisément parce qu'il est vide ! Donc aucune règle satisfaisant la propriété de la sous-formule (selon laquelle le séquent conclusion contient toutes les formules des séquents prémisses) ne peut se conclure par le séquent vide. Dans la mesure où toutes les règles satisfont cette propriété à l'exception de la coupure, on en déduit que si l'on peut démontrer le séquent vide, ce ne peut être qu'à partir de la règle de coupure.

Or l'élimination des coupures montre précisément que la règle de coupure n'est jamais nécessaire : on peut toujours remplacer une démonstration avec coupure par une démonstration sans coupure[5]. D'après ce qui précède, cela signifie en particulier que le séquent vide n'est pas démontrable, et plus généralement que le calcul des séquents ne contient aucune contradiction.

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 en utilisant un principe d'induction jusqu'à l'ordinal dénombrable ε0[6].

Notes et références[modifier | modifier le code]

  1. Gerhard Gentzen (trad. R. Feys et J. Ladrière), Recherches sur la déduction logique [« Untersuchungen über das logische schließen »], Presses Universitaires de France,‎ 1955
    Traduit et commenté
  2. Gerhard Gentzen, « Untersuchungen über das logische Schließen. II », Mathematische Zeitschrift, vol. 39,‎ 1935, p. 405–431 (DOI 10.1007/BF01201363)
    manuscrit reçu en 1933
  3. Table unicode des Opérateurs mathématiques
  4. Gerhard Gentzen, « Untersuchungen über das logische Schließen. I », Mathematische Zeitschrift, vol. 39,‎ 1935, p. 176-210 (DOI 10.1007/BF01201353)
    manuscrit reçu en 1933
  5. Ce replacement a cependant le défaut qu'il remplace une démonstration courte par une démonstration longue et même très longue!
  6. Ce qui ne donne pas une véritable preuve de la cohérence de l'arithmétique, car cette théorie, si elle est cohérente ne peut être démontrée telle en vertu des théorèmes d'incomplétude de Gödel

Bibliographie[modifier | modifier le code]

  • Jean-Yves Girard, Le Point aveugle, Tome I, chapitre 3 : "Les séquents classiques : LK", pp. 45-74. Ed. Hermann, mai 2006.
  • René David, Karim Nour, Christophe Raffali, Introduction à la logique, théorie de la démonstration 2001, Dunod, (ISBN 2100067966), chap. 5