UP | HOME

Logiques - Déduction naturelle, calcul des séquents

Table of Contents

1 Notation - Avertissement

Pour définir formellement des éléments syntaxiques, on utilise la notation de Backus-Naur. Par la suite, on pourra utiliser plusieurs règles pour définir un non-terminal, plutôt qu'une seule contenant toutes les alternatives : conformément à la norme ISO, il est recommandé de l'annoncer puisque "it is more difficult to understand a language if there are several syntax-rules defining a meta-identifier and no indication that each definition only partly defines the non-terminal symbol".

Cette convention permet notamment de définir des sous-ensembles en restreignant les règles utilisées.

sous-ensemble 1  X ::= règles 1 (utilisant X)
sous-ensemble 2  X ::= règles 2 (utilisant X)

Le sous-ensemble 1 est engendré par les règles 1, de même pour le sous-ensemble 2. L'ensemble engendré par X est produit par la réunion des règles 1 et 2.

ensemble complet X ::= règles 1 | règles 2 (utilisant X)

2 Logique en Coq

Il est possible en Coq de définir des types et des termes dans un langage fonctionnel évolué. Mais il est aussi possible d'interagir avec l'outil en adoptant le point de vue logique et procéder ainsi :

  • définir des types, vus comme des propositions,
  • construire en interaction des termes, vus comme des preuves, en utilisant des tactiques.

Bien sûr, cette pratique interactive est naturelle pour les types de la sorte Prop, qui correspond aux propositions. Mais elle est aussi utilisable pour des types représentant des données ou des calculs, de la sorte Type.

Cette pratique interactive reposant sur le point de vue logique a plusieurs avantages :

  • elle permet de programmer en étant détaché de la syntaxe, et en exprimant ses intentions, à l'aide des tactiques,
  • elle permet de composer les calculs et les raisonnements, et ainsi de calculer en vérifiant des propriétés,
  • elle peut conduire à des automatisations, par des tactiques recherchant automatiquement des preuves.

Lorsqu'on rentre dans ce mode interactif d'élaboration de preuves, après avoir défini un type, l'utilisateur est confronté à un but, exprimé sous la forme d'un séquent dit intuitionniste : une conjonction d'hypothèses H, un unique but, B. En logique, un tel séquent est représenté ainsi : H ⊢ B. Les interfaces habituelles de Coq présentent le séquent ainsi.

(* hypothèses *) 
h1 : H1
h2 : H2
...
============================
B (* but *)

L'utilisateur doit alors entrer des tactiques, l'outil se chargeant de construire progressivement la preuve à partir des tactiques. La preuve est exprimée en utilisant un système d'inférence particulier, appelé la déduction naturelle. Ce système correspond à un style naturel de raisonnement, en chaînage avant, allant des hypothèses vers le but. Il n'est cependant pas adapté au mode interactif, qui implique un chaînage arrière : de la conclusion (le but avec ses hypothèses) vers les prémisses (les sous-buts avec leurs hypothèses). Dans cette situation, c'est plutôt le calcul des séquents qui est utile. Ce système d'inférence repose sur des règles symétriques, et la décomposition des opérateurs logiques, dans le but ou dans les hypothèses formant le séquent.

Nous présentons ci-dessous les deux systèmes, inventés par Gentzen en 1934 :

  • la déduction naturelle,
  • le calcul des séquents.

Une bonne maîtrise de ces deux systèmes facilite l'apprentissage de Coq.

3 La logique propositionnelle

La logique propositionnelle forme le noyau des logiques ; aussi appelée calcul propositionnel ou calcul des propositions, elle est entendue comme la logique d'ordre zéro (sans quantification). Comme elle permet d'inférer des propositions dans un cadre fini, elle forme une logique décidable. Il existe ainsi des algorithmes permettant de déterminer si une proposition est prouvable, ou vraie. De plus la logique est complète : une proposition est prouvable si et seulement si elle est vraie dans toute interprétation sémantique. Par interprétation sémantique, on entend une interprétation booléenne, où une proposition atomique est interprétée par Vrai ou Faux. Le point de vue sémantique est particulièrement utile pour réfuter une proposition : il suffit en effet de trouver une interprétation sémantique dans laquelle la proposition est fausse. Cependant, ce point de vue a des limites : les interprétations ne sont simples qu'en logique classique, alors que nous nous intéressons à une logique intuitionniste. Pour la réfutation, une alternative est d'utiliser le calcul des séquents. Il existe aussi une interprétation sémantique en termes d'ensembles de preuves : c'est l'interprétation de Brouwer-Heyting-Kolmogorov, appelée par la suite interprétation probatoire (un qualificatif inventé pour ce cours et donc inusité, mais préféré à l'abréviation BHK).

Avant de détailler les deux systèmes d'inférence les plus utilisés, donnons un exemple pour saisir la différence entre la prouvabilité dans un système d'inférence et le vérité dans toute interprétation sémantique. Son étude peut être réservée à une seconde lecture.

Exemple : le tiers exclus A ∨ ¬A

  • interprétation sémantique
    • A vrai : A ∨ ¬A vrai
    • A faux : A ∨ ¬A vrai (car ¬A vrai)
    • conclusion : dans toute interprétation sémantique, A ∨ ¬A est vrai.
  • prouvabilité (dans le calcul des séquents, décrit ci-dessous)

    A ⊢ A
    ----------
    A ⊢ A ∨ ¬A
    ------------
    ⊢ ¬A, A ∨ ¬A
    ----------------
    ⊢ A ∨ ¬A, A ∨ ¬A
    ----------------
    ⊢ A ∨ ¬A
    
  • Les algorithmes de décision généralisent les approches suivies dans cet exemple : soit ils calculent toutes les interprétations possibles, soit ils recherchent automatiquement une preuve.
  • Le tiers exclus est une propriété prouvable et toujours vraie en logique classique. Elle ne peut être prouvée en logique intuitionniste : les séquents intuitionnistes ne comportant qu'un seul but interdisent la preuve précédente. Il est facile de voir par ailleurs qu'aucune autre preuve n'est possible.
  • Les interprétations sémantiques de la logique intuitionniste sont beaucoup moins intuitives que les interprétations booléennes : la réfutation du tiers exclus n'est pas immédiate.
  • L'interprétation par des ensembles de preuves est plus convaincante : les preuves de A ∨ ¬A forment la réunion disjointe des preuves de A et des preuves de ¬A. Sans information sur A, ces deux ensembles sont vides. L'exemple du tiers exclus montre qu'en logique classique, cette propriété n'est pas vérifiée.

3.1 Propositions

  • Les propositions se forment à partir d'atomes (dont le vrai et le faux) et les opérateurs logiques classiques. La logique est donc paramétrée par les propositions atomiques.

          atome A ::= A1 | ... (propositions atomiques) 
    proposition p ::= V | F | A (vrai | faux | atomes)
    		| p ∨ p | p ∧ p | ¬p | p -> q (disjonction | conjonction | négation | implication)
    
  • Aucun quantificateur n'est considéré. La logique du premier ordre ajoute des quantifications sur des individus, celle du second ordre des quantifications sur des prédicats, celle d'ordre supérieur des quantifications de tout ordre.

3.2 Séquents

  • Un séquent représente une déduction : en supposant une conjonction d'hypothèses, est déduite une disjonction de buts. Un séquent intuitionniste possède au plus un but.

    hypothèses              Γ ::= ∅ | p, Γ (liste de propositions, éventuellement vide)
    buts                    Δ ::= ∅ | p, Δ (liste de propositions, éventuellement vide)
    séquent classique      sc ::= Γ ⊢ Δ (en supposant la conjonction Γ, est déduit la disjonction Δ)
    séquent intuitionniste si ::= Γ ⊢ p (en supposant la conjonction Γ, est déduit la proposition p)
    			    | Γ ⊢   (en supposant la conjonction Γ, n'est rien déduit)
    
  • Une conjonction vide correspond au vrai, une disjonction vide correspond au faux : ce sont les éléments neutres de la conjonction et de la disjonction respectivement.
  • Une conjonction comprenant le faux est fausse, et une disjonction comprenant le vrai est vraie : ce sont les éléments absorbants de la conjonction et de la disjonction respectivement.
  • Il est utile d'introduire un système d'inférence définissant la bonne formation des propositions et des séquents. Comme aux ordres supérieurs, ce système sera étendu en un véritable système de types, on écrit les jugements sous la forme d'un jugement de typage, Γ ⊢ p : Prop pour affirmer que la proposition p est bien formée, ou Γ ⊢ Γ' : Prop∗, pour affirmer que les propositions dans Γ' sont bien formées. L'environnement Γ ne sert pas à ce stade : par la suite, il contiendra en plus de propositions des déclarations de variables, indispensables pour typer.

      Γ ⊢ p1 : Prop ...
    ---------------------- (Op opérateur logique, arité 0, 1 ou 2)
    Γ ⊢ (Op p1 ...) : Prop 
    
    		  Γ1 ⊢ p : Prop   Γ1 ⊢ Γ2 : Prop* 
    -------------     ------------------------------- 
    Γ ⊢ ∅ : Prop*          Γ1 ⊢ p, Γ2 : Prop*
    

3.3 Déduction naturelle

La déduction naturelle est adaptée à un raisonnement à partir des hypothèses. Elle s'appuie sur des figures naturelles du raisonnement comme celles-ci :

  • par hypothèse,
  • "ex falso sequitur quodlibet" : du faux tout s'ensuit,
  • par contradiction,
  • par analyse des cas d'une alternative.

La présentation habituelle de la déduction naturelle (par exemple celle dans Wikipedia) met en avant ce mouvement des hypothèses vers le but dans les démonstrations. Ce n'est pas la présentation que nous donnons ici. Fondée sur des séquents intuitionnistes, elle vise à mettre en avant la correspondance (dite de Curry-Howard) entre la déduction naturelle et la programmation fonctionnelle, fondée sur une série d'isomorphismes.

Logique Programmation
proposition type
preuve terme
système d'inférence système de types
normalisation des preuves exécution des termes

La logique considérée est intuitionniste. Pour obtenir une logique classique, il est nécessaire d'ajouter un axiome, équivalent au tiers exclus. La correspondance peut être étendue à un tel axiome, en utilisant des opérateurs de contrôle, permettant de capturer la continuation courante (une abstraction de la pile d'exécution).

3.3.1 Les règles

Les règles logiques se répartissent en des des règles d'introduction (de suffixe I), qui introduisent un opérateur logique, et des règles d'élimination (de suffixe E), qui les détruisent. Les commentaires expliquant les règles suivent le chaînage avant dans leur formulation : si on a les prémisses, alors on a la conclusion. On utilise le verbe "déduire" pour parler du but, et le verbe "supposer" pour parler des hypothèses ; toutes les choses sont supposées égales par ailleurs lorsqu'elles ne sont pas précisées. Le système d'inférence définit la validité de séquents intuitionnistes Γ ⊢ p, en utilisant des jugements de bonne formation Γ ⊢ q : Prop ou Γ ⊢ Γ' : Prop∗. Les hypothèses de bonne formation visent à garantir que la validité du séquent Γ ⊢ p entraîne que Γ ⊢ p, Γ : Prop∗, c'est-à-dire que p et Γ sont bien formés.

3.3.1.1 Axiome : preuve par hypothèse
  • [Hyp] : En supposant p, p est déduit.

    Γ1, p, Γ2 ⊢ Γ1, p, Γ2 : Prop*  
    ----------------------------- [Hyp]
    	Γ1, p, Γ2 ⊢ p
    
3.3.1.2 Règles logiques
  • [F-E] : Si Faux est déduit, n'importe quelle proposition est déduite.
  • [V-I] : Vrai est toujours déduit.

    Γ ⊢ F  Γ ⊢ p : Prop        Γ ⊢ Γ : Prop
    ------------------- [F-E]  ------------ [V-I]   
           Γ ⊢ p                  Γ ⊢ V
    
  • [∧-Eg], [∧-Ed] : Si p ∧ q et déduit, alors p est déduit et alors q est déduit.
  • [∨-Ig], [∨-Id] : Si p est déduit ou si q est déduit, alors p ∨ q est déduit.
  • [∧-I] : Si p est déduit et q est déduit, alors p ∧ q est déduit.
  • [∨-E] : Si

    • p ∨ q est déduit,
    • en supposant p est déduit r et
    • en supposant q est déduit r,

    alors r est déduit.

      Γ ⊢ p ∧ q                 Γ ⊢ p    Γ ⊢ q : Prop
    ------------ [∧-Eg]         --------------------- [∨-Ig]   
       Γ ⊢ p                         Γ ⊢ p ∨ q
    
      Γ ⊢ p ∧ q                 Γ ⊢ q    Γ ⊢ p : Prop
    ------------[∧-Ed]          --------------------- [∨-Id]   
       Γ ⊢ q                         Γ ⊢ p ∨ q
    
    	   q, Γ ⊢ r
    Γ ⊢ p ∨ q  p, Γ ⊢ r          Γ ⊢ p   Γ ⊢ q
    ------------------- [∨-E]   --------------- [∧-I]   
          Γ ⊢ r                    Γ ⊢ p ∧ q
    
  • [¬-E] : Si ¬p est déduit et p est déduit (une contradiction), alors Faux est déduit.
  • [¬-I] : Si en supposant p est déduit Faux, alors ¬p est déduit.

    Γ ⊢ ¬p  Γ ⊢ p                 p, Γ ⊢ F
    ------------- [¬-E]         ------------ [¬-I]   
       Γ ⊢ F                      Γ ⊢ ¬p
    
  • [->-E] : Si p -> q est déduit et p est déduit, alors q est déduit.
  • [->-I] : Si en supposant p est déduit q, alors p -> q est déduit.

    Γ ⊢ p -> q   Γ ⊢ p            p, Γ ⊢ q 
    ------------------ [->-E]   ------------ [->-I]
        Γ ⊢ q                    Γ ⊢ p -> q
    

3.4 Calcul des séquents

Le calcul des séquents est adapté à un raisonnement en chaînage arrière (de la conclusion vers les prémisses). La recherche de preuves est ainsi facilitée puisque le calcul s'appuie sur la décomposition des opérateurs logiques, à gauche ou à droite du séquent. La règle de coupure est la seule exception qui demande de deviner une proposition (voir la proposition p de la règle [Coupure] ci-dessous). Heureusement, il est possible de se dispenser de cette règle : le système sans cette règle est équivalent au système avec cette règle. C'est une propriété fondamentale, dite d'élimination des coupures, qui rend possible la recherche automatique de preuves. C'est une situation bien différente de celle de la déduction naturelle où de nombreuses règles d'élimination demandent de deviner une proposition, compromettant l'automatisation en chaînage arrière. En pratique, la règle de coupure sert à rendre modulaire les preuves : il s'agit d'une généralisation de la transitivité de la déduction ou de la règle du modus ponens.

Le calcul des séquents fournit un système d'inférence applicable à la logique classique ou à la logique intuitionniste. La différence concerne la forme des séquents :

  • logique classique : séquents classiques, à buts multiples (sous la forme d'une disjonction),
  • logique intuitionniste : séquents intuitionnistes. à but unique ou sans but.

En Coq, on utilise une logique intuitionniste, correspondant à un point de vue constructiviste, calculatoire. Les séquents ont donc au plus un but. C'est pourquoi nous commençons par les règles intuitionnistes. De plus, elles sont sans doute plus intuitives, et pour moitié identiques à celles de la déduction naturelle.

Les règles logiques se classent en règles à gauche (de suffixe G) et à droite (de suffixe D). Les règles à droite correspondent aux règles d'introduction de la déduction naturelle. Un seul axiome est présent : l'identité. Enfin, des règles administratives permettent de traiter les listes comme des ensembles de propositions. Les commentaires expliquant les règles suivent le chaînage arrière dans leur formulation : on a la conclusion si on a les prémisses. On utilise le verbe "déduire" pour parler du but, et le verbe "supposer" pour parler des hypothèses ; toutes les choses sont supposées égales par ailleurs lorsqu'elles ne sont pas précisées. Les hypothèses en conjonction sont reliées par et et les buts en disjonction sont reliées par ou, et leur composition reste au singulier, pour exprimer leur unité.

3.4.1 Les règles intuitionnistes

Comme la déduction naturelle, le système d'inférence définit la validité de séquents intuitionnistes Γ ⊢ p, en utilisant les jugements de bonne formation Γ ⊢ q : Prop ou Γ ⊢ Γ' : Prop∗. Les hypothèses de bonne formation visent à garantir que la validité du séquent Γ ⊢ p entraîne que Γ ⊢ p, Γ : Prop∗, c'est-à-dire que p et Γ sont bien formés.

3.4.1.1 Identité et coupure
  • [Id] : En supposant p est déduit p.
  • [Coupure] : En supposant Γ1 et Γ2 est déduit q s'il existe p (la coupure) telle qu'en supposant Γ1 est déduit p et en supposant p et Γ2 est déduit q.

    ⊢ p : Prop                    Γ1 ⊢ p   p, Γ2 ⊢ q
    ---------- [Id]               ------------------ [Coupure]
      p ⊢ p                          Γ1, Γ2 ⊢ q
    

Remarque : la règle de coupure peut être vue comme une instance de la règle [->-G], avec l'implication p -> p, soit l'identité, confondue avec Vrai, l'élément neutre de la conjonction, et ainsi omise.

3.4.1.2 Règles logiques
  • [F-G] : Du Faux est déduit la disjonction vide (qui correspond au Faux).
  • [V-D] : De la conjonction vide (qui correspond au Vrai), est déduit Vrai.
  • [F-D] : Faux est déduit si rien n'est déduit.
  • [V-G] : Vrai et Γ est supposé si Γ est supposé.

    ------ [F-G]                ----- [V-D]   
     F ⊢                         ⊢ V
    
       Γ ⊢ p                      Γ ⊢ 
    ----------- [V-G]           ------- [F-D]
     V, Γ ⊢ p                    Γ ⊢ F
    
  • [∧-Gg], [∧-Gd] : p ∧ q et Γ est supposé si p et Γ est supposé ou si q et Γ est supposé.
  • [∨-Dg], [∨-Dd] : p ∨ q est déduit si p est déduit ou si q est déduit.
  • [∧-D] : p ∧ q est déduit si p est déduit et q est déduit.
  • [∨-G] : p ∨ q et Γ est supposé si p et Γ est supposé et q et Γ est supposé.

    p, Γ ⊢ r   Γ ⊢ q : Prop           Γ ⊢ p   Γ ⊢ q : Prop
    ----------------------- [∧-Gg]    -------------------- [∨-Dg]   
        p ∧ q, Γ ⊢ r                        Γ ⊢ p ∨ q
    
    q, Γ ⊢ r   Γ ⊢ p : Prop           Γ ⊢ q   Γ ⊢ p : Prop
    ----------------------- [∧-Gd]    -------------------- [∨-Dd]   
        p ∧ q, Γ ⊢ r                        Γ ⊢ p ∨ q
    
    p, Γ ⊢ r   q, Γ ⊢ r               Γ ⊢ p   Γ ⊢ q
    ------------------- [∨-G]         ------------- [∧-D]   
       p ∨ q, Γ ⊢ r                     Γ ⊢ p ∧ q
    
  • [¬-G] : En supposant ¬p et Γ rien n'est déduit si en supposant Γ est déduit p.
  • [¬-D] : En supposant Γ est déduit ¬p si en supposant p et Γ rien n'est déduit.

      Γ ⊢ p                    p, Γ ⊢ 
    ---------- [¬-G]          -------- [¬-D]   
     ¬p, Γ ⊢                   Γ ⊢ ¬p
    
  • [->-G] : En supposant p -> q, Γ1 et Γ2 est déduit r si en supposant Γ1 est déduit p et en supposant q et Γ2 est déduit r.
  • [->-D] : En supposant Γ est déduit p -> q si en supposant p et Γ est déduit q.

    Γ1 ⊢ p     q, Γ2 ⊢ r            p, Γ ⊢ q
    -------------------- [->-G]   ------------ [->-D]
     p -> q, Γ1, Γ2 ⊢ r            Γ ⊢ p -> q
    
3.4.1.3 Règles structurelles (A := Affaiblissement, C := Contraction, P := Permutation)
  • [A-G] : p et Γ est supposé si Γ est supposé.
  • [A-D] : p est déduit si rien n'est déduit.
  • [A-G], [A-D], [C-G], [P-G] : les hypothèses se comportent comme des ensembles, et non des listes. Le nombre d'occurrences n'importe pas, ni l'ordre.

    Γ ⊢ q   Γ ⊢ p : Prop            Γ ⊢    Γ ⊢ p : Prop 
    -------------------- [A-G]      ------------------- [A-D]   
         p, Γ ⊢ q                         Γ ⊢ p
    
     p, p, Γ ⊢ q               
    ------------ [C-G]         
      p, Γ ⊢ q                 
    
       Γ ⊢ q                     
    ------------ [P-G] (σ : permutation)        
      Γ[σ] ⊢ q
    

Remarque 1 : les noms de ces règles reposent sur un chaînage avant.

Remarque 2 : la règle d'affaiblissement à droite peut s'interpréter ainsi :

  • toute proposition est déduite si le faux (correspondant au but vide) est déduit.

3.4.2 Les règles classiques

Après la logique intuitionniste, intéressons-nous à la logique classique. Cette partie peut être laissée à une seconde lecture, d'une part pour simplifier, d'autre part pour se concentrer sur la logique sous-jacente à Coq, qui est intuitionniste. Il reste que la différence conceptuelle entre les deux systèmes, classique et intuitionniste, est minime : les règles pour la logique intuitionniste constituent une restriction des règles pour la logique classique, en imposant que les séquents ont au plus un but, alors que les séquents classiques utilisent une disjonction de buts.

Voici un exemple utilisant cette possibilité de buts multiples pour montrer le tiers exclus. En logique intuitionniste, cette proposition ne peut pas être démontrée.

----- [Id]
A ⊢ A
---------- [∨-Dg]
A ⊢ A ∨ ¬A
------------ [¬-D]
⊢ ¬A, A ∨ ¬A
---------------- [∨-Dd]
⊢ A ∨ ¬A, A ∨ ¬A
---------------- [C-D]
⊢ A ∨ ¬A

Le tiers exclus marque la ligne de partage entre la logique intuitionniste et la logique classique. Par exemple, si on l'ajoute comme axiome à la déduction naturelle, alors on obtient la logique classique.

3.4.2.1 Identité et coupure
  • [Id] : En supposant p est déduit p.
  • [Coupure] : En supposant Γ1 et Γ2 est déduit Δ1 ou Δ2 s'il existe p (la coupure) telle qu'en supposant Γ1 est déduit p ou Δ1 et en supposant p et Γ2 est déduit Δ2.

    Γ ⊢ p : Prop              Γ1 ⊢ p, Δ1   p, Γ2 ⊢ Δ2
    ------------ [Id]         ----------------------- [Coupure]
       p ⊢ p                      Γ1, Γ2 ⊢ Δ1, Δ2
    
3.4.2.2 Règles logiques
  • [F-G] : Du Faux est déduit la disjonction vide (qui correspond au Faux).
  • [V-D] : De la conjonction vide (qui correspond au Vrai), est déduit Vrai.
  • [F-D] : Faux ou Δ est déduit si Δ est déduit.
  • [V-G] : Vrai et Γ est supposé si Γ est supposé.

    ------ [F-G]                ----- [V-D]   
     F ⊢                         ⊢ V
    
       Γ ⊢ Δ                      Γ ⊢ Δ
    ----------- [V-G]           ---------- [F-D]
     V, Γ ⊢ Δ                    Γ ⊢ F, Δ
    
  • [∧-Gg], [∧-Gd] : p ∧ q et Γ est supposé si p et Γ est supposé ou si q et Γ est supposé.
  • [∨-Dg], [∨-Dd] : p ∨ q ou Δ est déduit si p ou Δ est déduit ou si q ou Δ est déduit.
  • [∧-D] : p ∧ q ou Δ est déduit si p ou Δ est déduit et q ou Δ est déduit.
  • [∨-G] : p ∨ q et Γ est supposé si p et Γ est supposé et q et Γ est supposé.

    p, Γ ⊢ Δ   Γ ⊢ q : Prop           Γ ⊢ p, Δ   Γ ⊢ q : Prop
    ----------------------- [∧-Gg]    ----------------------- [∨-Dg]   
         p ∧ q, Γ ⊢ Δ                      Γ ⊢ p ∨ q, Δ
    
    q, Γ ⊢ Δ   Γ ⊢ p : Prop           Γ ⊢ q, Δ   Γ ⊢ p : Prop
    ----------------------- [∧-Gd]    ----------------------- [∨-Dd]   
         p ∧ q, Γ ⊢ Δ                      Γ ⊢ p ∨ q, Δ
    
    p, Γ ⊢ Δ   q, Γ ⊢ Δ               Γ ⊢ p, Δ   Γ ⊢ q, Δ
    ------------------- [∨-G]         ------------------- [∧-D]   
       p ∨ q, Γ ⊢ Δ                        Γ ⊢ p ∧ q, Δ
    
  • [¬-G] : En supposant ¬p et Γ est déduit Δ si en supposant Γ est déduit p ou Δ.
  • [¬-D] : En supposant Γ est déduit ¬p ou Δ si en supposant p et Γ est déduit Δ.

     Γ ⊢ p, Δ                p, Γ ⊢ Δ
    --------- [¬-G]          --------- [¬-D]   
    ¬p, Γ ⊢ Δ                Γ ⊢ ¬p, Δ
    
  • [->-G] : En supposant p -> q et Γ est déduit Δ si en supposant Γ est déduit p ou Δ et en supposant q et Γ est déduit Δ.
  • [->-D] : En supposant Γ est déduit p -> q ou Δ si en supposant p et Γ est déduit q ou Δ.

    Γ ⊢ p, Δ   q, Γ ⊢ Δ          p, Γ ⊢ q, Δ
    ------------------- [->-G]  ------------- [->-D]
       p -> q, Γ ⊢ Δ            Γ ⊢ p -> q, Δ
    
3.4.2.3 Règles structurelles (A := Affaiblissement, C := Contraction, P := Permutation)
  • [A-G] : p et Γ est supposé si Γ est supposé.
  • [A-D] : p et Δ est déduit si Δ est déduit.
  • [A-G], [A-D], [C-G], [C-D], [P-G], [P-D] : les hypothèses et les buts se comportent comme des ensembles, et non des listes. Le nombre d'occurrences n'importe pas, ni l'ordre.

    Γ ⊢ Δ   Γ ⊢ p : Prop           Γ ⊢ Δ   Γ ⊢ p : Prop
    -------------------- [A-G]     -------------------- [A-D]   
          p, Γ ⊢ Δ                       Γ ⊢ p, Δ
    
     p, p, Γ ⊢ Δ                 Γ ⊢ p, p, Δ
    ------------ [C-G]          ------------ [C-D]   
      p, Γ ⊢ Δ                    Γ ⊢ p, Δ
    
     Γ ⊢ Δ           Γ ⊢ Δ
    -------- [P-G]  -------- [P-D] (σ : permutation)   
    Γ[σ] ⊢ Δ        Γ ⊢ Δ[σ]
    

Remarque : les noms de ces règles reposent sur un chaînage avant.

3.4.3 Quelques variantes

La règle de coupure peut être présentée sans partition des environnements Γ et Δ. Il est facile de dériver l'une de l'autre en utilisant les règles structurelles.

Coupure - Variante

Γ ⊢ p, Δ    p, Γ ⊢ Δ
-------------------- [Coupure']
       Γ ⊢ Δ

De même pour l'implication gauche.

Implication gauche - Variante

Γ ⊢ p, Δ   q, Γ ⊢ Δ        
------------------- [->-G']
   p -> q, Γ ⊢ Δ

Dérivabilité des règles de coupure et d'implication à gauche - Nouvelle règle dans l'ancien système / ancienne règle dans le nouveau système

Γ ⊢ p, Δ    p, Γ ⊢ Δ         Γ1, ⊢ p, Δ1              p, Γ2 ⊢ Δ2 
--------------------         ----------- [A-G+A-D]*   ---------- [A-G+A-D]*    
Γ, Γ ⊢ Δ, Δ                  Γ1, Γ2 ⊢ p, Δ1, Δ2       p, Γ1, Γ2 ⊢ Δ1, Δ2 
----------- [C-G+C-D]*       -------------------------------------------
Γ ⊢ Δ                        Γ1, Γ2 ⊢ Δ1, Δ2


Γ ⊢ p, Δ    q, Γ ⊢ Δ                Γ1, ⊢ p, Δ1              q, Γ2 ⊢ Δ2 
--------------------                ----------- [A-G+A-D]*   ---------- [A-G+A-D]*    
p -> q, Γ, Γ ⊢ Δ, Δ                 Γ1, Γ2 ⊢ p, Δ1, Δ2       q, Γ1, Γ2 ⊢ Δ1, Δ2 
------------------- [C-G+C-D]*      -------------------------------------------
p -> q, Γ ⊢ Δ                       p -> q, Γ1, Γ2 ⊢ Δ1, Δ2

Avec la nouvelle règle de coupure [Coupure'], les règles de contraction deviennent inutiles.

Dérivabilité des règles de contraction - Ancienne règle dans le nouveau système

----- [A-G+A-D]*                              ----- [A-G+A-D]*
p, Γ ⊢ p, Δ     p, p, Γ ⊢ Δ     Γ ⊢ p, p, Δ   p, Γ ⊢ p, Δ   
---------------------------     ------------------------- 
p, Γ ⊢ Δ                        Γ ⊢ p, Δ

L'axiome [Id] peut intégrer les affaiblissements.

p, Γ ⊢ p, Δ : Prop*     
------------------- [Id']         
   p, Γ ⊢ p, Δ

Dans ce cas, les règles d'affaiblissement deviennent inutiles. Les règles d'affaiblissement ne sont pas dérivables : elles sont seulement admissibles. En effet, on peut montrer par induction sur Γ ⊢ Δ que p, Γ ⊢ Δ et Γ ⊢ p, Δ peuvent être prouvés. Il suffit de rajouter p à chaque jugement dans la preuve et d'utiliser une permutation.

Les règles [∧-Gg] et [∧-Gd] peuvent être fusionnées en une seule règle, [∧-G], montrant ainsi directement l'interprétation de la liste de formules comme une conjonction à gauche. De même pour les règles [∨-Dg] et [∨-Dd].

p, q, Γ ⊢ Δ            Γ ⊢ p, q, Δ            
------------ [∧-G']    ------------ [∨-D'] 
p ∧ q, Γ ⊢ Δ           Γ ⊢ p ∨ q, Δ

Dérivabilité des règles pour la conjonction et la disjonction - Nouvelle règle dans l'ancien système / ancienne règle dans le nouveau système

p, q, Γ ⊢ Δ         
---------------
p, p ∧ q, Γ ⊢ Δ          p, Γ ⊢ Δ
-------------------      -----------
p ∧ q, p ∧ q, Γ ⊢ Δ      p, q, Γ ⊢ Δ   
-----------              ------------
p ∧ q, Γ ⊢ Δ             p ∧ q, Γ ⊢ Δ                 

Γ ⊢ p, q, Δ         
---------------
Γ ⊢ p, p ∨ q, Δ          Γ ⊢ p, Δ
-------------------      -----------
Γ ⊢ p ∨ q, p ∨ q, Δ      Γ ⊢ p, q, Δ   
-----------              ------------
Γ ⊢ p ∨ q, Δ             Γ ⊢ p ∨ q, Δ

Avec ces nouvelles règles, sans les règles de contraction ni d'affaiblissement, sans la règle de coupure, qui n'est pas dérivable mais admissible, il devient possible de décider si un séquent est valide ou non : il suffit de décomposer à gauche et à droite, jusqu'à obtenir l'identité modifiée [Id'] ou non. Les règles du nouveau système n'imposent en effet aucun choix et vérifient la propriété de la sous-formule : le multi-ensemble des formules et sous-formules d'une prémisse est inclus dans celui de la conclusion, ce qui assure la convergence.

3.4.4 Point de vue algébrique

Les règles logiques du calcul des séquents ont clairement une inspiration algébrique. En chaînage arrière, elles peuvent être vues comme des simplifications suivant des équations algébriques. Elles reposent aussi sur l'interprétation de la relation de déduction par une relation d'ordre, qui mesurerait le degré de vérité. Les règles peuvent alors être interprétées comme des propriétés d'une structure algébrique ordonnée. Dans le cas simple où les opérateurs logiques sont la conjonction et la disjonction, cette structure est une algèbre de Boole.

Au préalable, il est nécessaire de retrouver l'interprétation algébrique des listes de formules à gauche et à droite, à savoir que la liste des hypothèses est une conjonction et la liste des buts une disjonction. C'est exactement le sens des deux règles dérivables [∧-G'] et [∨-D'].

p, q, Γ ⊢ Δ            Γ ⊢ p, q, Δ            
------------ [∧-G']    ------------ [∨-D'] 
p ∧ q, Γ ⊢ Δ           Γ ⊢ p ∨ q, Δ

Autrement dit, la virgule séparant les éléments de la liste correspond à l'opérateur à gauche et à droite.

Pour illustrer cette interprétation, associons des règles à quelques propriétés algébriques.

  • Neutralité de Vrai et Faux pour la conjonction et la disjonction : règles [V-G] et [F-D]
  • Distributivité de la conjonction sur la disjonction, disjonction comme borne supérieure : règle [∨-G]
  • Distributivité de la disjonction sur la conjonction, conjonction comme borne inférieure : règle [∧-D]

4 La logique du premier ordre

La logique du premier ordre, appelée aussi calcul des prédicats, étend la logique propositionnelle (ou d'ordre zéro) en autorisant la paramétrisation des propositions et la quantification de ces paramètres. Un prédicat est une proposition paramétrée par une ou plusieurs variables.

Utilisant des variables pouvant parcourir des ensembles infinis, comme les entiers naturels, la logique du premier ordre est beaucoup plus puissante, expressive, que celle propositionnelle. A vrai dire, toutes les mathématiques peuvent s'écrire avec une logique du premier ordre, en utilisant la théorie des ensembles. Cependant, comme la logique propositionnelle, c'est une logique complète : une proposition est prouvée si et seulement elle est vérifiée dans tout modèle. Un modèle (classique) interprète

  • les domaines des variables par des ensembles (non vides),
  • les opérateurs utilisés pour construire les termes appartenant aux domaines et pour calculer dans ces domaines par des fonctions, et
  • les prédicats par des relations.

Si la logique est complète, en revanche, toute théorie cohérente et suffisamment expressive est incomplète au sens suivant : il existe une proposition qui ne peut être ni prouvée ni réfutée dans cette théorie. Comme la logique est complète, on déduit qu'il existe plusieurs modèles de cette théorie, les uns vérifiant la proposition, les autres non. Par exemple, à côté du modèle standard de l'arithmétique, fondé sur les entiers naturels, il existe des modèles non standards. Cette incomplétude est un premier résultat fâcheux : le gain de puissance se fait au détriment de la complétude et de l'univocité sémantique, appelée catégoricité. De plus, elle est sans remède : une théorie suffisamment expressive n'est pas décidable algorithmiquement. En conséquence, la démonstration automatique doit limiter ses ambitions. Enfin, un dernier résultat rend vain nos espoirs de certitude :

  • parmi ces propositions ni prouvables ni réfutables, il en existe une qui exprime, moyennant un codage, la cohérence (la non-contradiction) de la théorie ; il est donc impossible de prouver mathématiquement que les mathématiques sont cohérentes, c'est-à-dire non contradictoires, plus concrètement qu'elles ne prouvent pas 0 = 1!

Ces résultats, non seulement fâcheux par les limitations qu'ils impliquent, mais aussi fameux, sont l'œuvre de logiciens célèbres :

Ils sont importants puisqu'ils s'appliquent directement à Coq :

  • il est impossible de décider si un type est habitable ou non,
  • la cohérence de Coq ne peut être démontrée en Coq.

Enfin, l'interprétation probatoire de la quantification universelle est fonctionnelle :

  • une preuve de ∀x. p est une fonction associant à tout x une preuve de p.

Comme p peut dépendre de x, cette fonction est plutôt une famille paramétrée par le domaine de x, de type un produit dépendant. La quantification existentielle correspond au type d'une somme dépendante :

  • une preuve de ∃x. p est un couple, formé d'un témoin t et d'une preuve de p[x := t].

4.1 Termes

  • Les termes sont définis de manière algébrique, à partir d'une signature déclarant les opérateurs.

    terme          t ::= x | (f t ... t) (variable | opérateur appliqué à des termes)
    type atomique TA ::= TA1 | ... 
    type           T ::= TA (types atomiques)
    		   | T -> T (type flèche) 
    signature      Γ ::= ∅ | (f : T), Γ  (liste de déclarations d'opérateurs)
    environnement  Γ ::= ∅ | (x : T), Γ (liste de déclarations de variables)
    
  • Un environnement et une signature définissent une relation fonctionnelle : à une variable ou à un opérateur, est associé au plus un type. Le système d'inférence suivant exprime cette propriété de bonne formation.

    Bonne formation des déclarations - Typage monomorphe

    	 Γ ⊢    z ∉ Γ    p ≠ (z : T)  z ∉ Γ    
    -----    ------------    ------------------    ------
     ∅ ⊢     (z : T), Γ ⊢       z ∉ (p, Γ)         z  ∉ ∅
    
  • Il existe une autre notion d'environnement, commune dans les langages de programmation, autorisant plusieurs déclarations d'une même variable : l'unique déclaration active est celle la plus haute dans la pile, autrement dit la dernière empilée. Notre approche permet de considérer l'environnement comme un ensemble, dont les éléments sont identifiés par le nom de la variable.
  • Le typage est défini par un système d'inférence. Le contexte de typage est constitué de la signature indiquant le type des opérateurs et de l'environnement qui déclare les variables apparaissant dans le terme.

    Typage - Paramétré par le type des termes TT et le type des opérateurs TO

       Γ1, (x : TT), Γ2 ⊢              Γ1, (f : TO), Γ2 ⊢ 
    --------------------------     --------------------------
    Γ1, (x : TT), Γ2  ⊢ x : TT     Γ1, (f : TO), Γ2  ⊢ f : TO
    
    Γ ⊢ f : TT -> TO   Γ ⊢ t : TT
    -----------------------------
           Γ ⊢ f t : TO
    
  • Le système de types défini au-dessus est tout à fait général. Au premier ordre, on se limite à des termes de type atomique et à des opérateurs produisant des types atomiques à partir de termes.

    Premier ordre

    type des opérateurs      TO ::= TT | TT -> TO
    type des termes          TT ::= TA
    

4.2 Propositions, séquents, typage au premier ordre

  • Aux propositions atomiques s'ajoutent des applications de prédicats à des termes, les prédicats étant déclarés dans une signature. Une proposition atomique peut être vue comme un prédicat appliqué à une liste vide de termes.

    prédicat    P ::= P_1 | ...        
    sorte       T ::= Prop (type correspondant aux propositions)
    signature   Γ ::= ∅ | (P : T), Γ (liste de déclarations de prédicats)
    atome       A ::= (P t ... t) (prédicat P appliqué à des termes t)                 
    proposition p ::= ∀(x : T). p | ∃(x : T). p (quantification universelle | existentielle)
    
  • Les séquents deviennent asymétriques : les hypothèses contiennent non seulement des propositions mais aussi l'environnement et la signature, déclarant les variables, les opérateurs et les prédicats.

    hypothèses              Γ ::= ∅ | p, Γ | (x : T), Γ | (f : T), Γ | (P : T), Γ
    			      (liste de propositions et de déclarations, éventuellement vide)
    buts                    Δ ::= ∅ | p, Δ (liste de propositions, éventuellement vide)
    séquent classique      sc ::= Γ ⊢ Δ (en supposant la conjonction Γ, est déduit la disjonction Δ)
    séquent intuitionniste si ::= Γ ⊢ p (en supposant la conjonction Γ, est déduit la proposition p)
    			    | Γ ⊢   (en supposant la conjonction Γ, n'est rien déduit)
    
  • Le système de types pour les termes peut être étendu aux propositions, puis aux hypothèses et aux buts. Il étend aussi et remplace le système définissant la bonne formation des propositions, utilisé en logique propositionnelle.

    Typage - Suite - Paramétré par le type des termes TT, le type des opérateurs TO et le type des prédicats TP

       Γ1, (P : TP), Γ2 ⊢  
    --------------------------   
    Γ1, (P : TP), Γ2  ⊢ P : TP   
    
    Γ ⊢ P : TT -> TP   Γ ⊢ t : TT
    -----------------------------
           Γ ⊢ P t : TP
    
    Γ ⊢ p1 : Prop ...
    ---------------------- (Op opérateur logique, arité 0, 1 ou 2)
    Γ ⊢ (Op p1 ...) : Prop 
    
    Γ1, (x : TT), Γ2 ⊢ p : Prop     Γ1, (x : TT), Γ2 ⊢ p : Prop
    ----------------------------    ----------------------------
    Γ1, Γ2 ⊢ ∀(x : TT). p : Prop    Γ1, Γ2 ⊢ ∃(x : TT). p : Prop
    
    -------------
    Γ ⊢ ∅ : Prop*
    
    Γ1 ⊢ p : Prop   Γ1 ⊢ Γ2 : Prop*    Γ1 ⊢ dec   Γ1 ⊢ Γ2 : Prop*
    -------------------------------    -------------------------- (dec ::= (x : TT) (f : TO) | (P : TP)) 
         Γ1 ⊢ p, Γ2 : Prop*               Γ1 ⊢ dec, Γ2 : Prop*
    
  • Au premier ordre, on se limite à des prédicats produisant des propositions à partir de termes.

    Premier ordre

    type des opérateurs      TO ::= TT | TT -> TO (rappel)
    type des termes          TT ::= TA (rappel)
    type des prédicats       TP ::= Prop | TT -> TP
    

4.3 Liaison des variables - Conventions

Les quantificateurs universels et existentiels sont des lieurs : ils lient la variable quantifiée à l'intérieur de la proposition. Ces lieurs sont analogues aux lieurs des langages de programmation comme les lambdas pour les fonctions anonymes. Comme pour les lambdas, le sens de la proposition n'est pas modifié si on renomme la variable liée par le quantificateur, à condition d'éviter toute capture de la nouvelle variable par un autre lieur imbriqué : autrement dit, l'ensemble des propositions est le quotient par la relation d'équivalence induite par le renommage (relation appelée alpha-conversion). Il n'est pas simple de traiter rigoureusement ce quotient, par exemple lorsqu'on implémente la logique du premier ordre en Coq. Cependant, dans la description des règles logiques, une convention suffit généralement pour simplifier le traitement des variables liées. Cette convention est d'ailleurs utilisée par l'analyseur syntaxique de Coq. Lorsqu'elle n'est plus respectée, un renommage s'impose pour la faire respecter.

Convention pour les variables libres et liées

Etant donné un ensemble fini d'expressions en considération, l'ensemble de leurs variables libres et l'ensemble de leurs variables liées sont supposés disjoints.

Si on veut typer la proposition ∀x.∀x.p, on s'aperçoit que la convention n'est pas respectée après l'introduction dans l'environnement du premier x , qui devient une variable libre. La proposition doit donc être renommée en ∀y.∀x.p : voir l'exemple en Coq, qui utilise le nom _ pour y, pour marquer l'absence d'utilisation de la variable. On introduit donc une seconde convention.

Convention pour les variables liées

Deux lieurs imbriqués lient des variables distinctes.

Ainsi, telles que nous les avons formulées, les règles de typage pour les quantificateurs ne permettent de typer que les propositions vérifiant cette convention. C'est pourquoi la règle plus rigoureuse utilisée pour le typage des quantificateurs autorise un renommage dans la prémisse, pour éviter cette restriction aux propositions respectant la convention.

Γ1, (y : TT), Γ2 ⊢ p[x:=y] : Prop    Γ1, (y : TT), Γ2 ⊢ p[x:=y] : Prop
---------------------------------    ---------------------------------
  Γ1, Γ2 ⊢ ∀(x : TT). p : Prop          Γ1, Γ2 ⊢ ∃(x : TT). p : Prop

Enfin, lors d'une substitution d'une variable x par un terme t dans une proposition p, notée p[x:=t], la convention garantit que les variables libres ne sont pas capturées. Si le terme contient lui-aussi des lieurs (ce qui n'est pas le cas au premier ordre), il se peut que le terme après substitution ne respecte pas la convention : un renommage est nécessaire.

4.4 Déduction naturelle

Les règles de la déduction naturelle sont étendues au cas des quantificateurs. Les conditions de typage, qui remplacent les conditions de bonne formation, visent à garantir que tout séquent valide Γ ⊢ p est bien typé, soit Γ ⊢ p, Γ : Prop∗. On le vérifie facilement par induction, en utilisant un lemme de préservation du typage pour les substitutions. Une seule règle doit être récrite, l'axiome [Hyp].

  • [Hyp] : En supposant p est déduit p.

     Γ1, p, Γ2 ⊢ Γ1, p, Γ2 : Prop*  
    ----------------------------- [Hyp]
    	Γ1, p, Γ2 ⊢ p
    
  • [∀-E] : Si ∀x. p est déduit, alors p[x := t] est déduit, après substitution à x de t.
  • [V-I] : Si en supposant x quelconque, p est déduit, alors ∀x. p est déduit.

    Γ ⊢ ∀(x : T). p   Γ ⊢ t : T         (x : T), Γ ⊢ p   Γ ⊢ Γ : Prop* 
    --------------------------- [∀-E]   ------------------------------ [∀-I]
          Γ ⊢ p[x := t]                      Γ ⊢ ∀(x : T). p
    
  • [∃-E] : Si

    • ∃x, p est déduit et
    • en supposant x quelconque vérifiant p, est déduit q,

    alors q est déduit.

  • [∃-I] : Si p est déduit après substitution à x de t, alors ∃x, p est déduit.

    Γ ⊢ ∃(x : T). p    Γ ⊢ q : Prop   
    	      (x : T), p, Γ ⊢ q         Γ ⊢ p[x := t]    Γ ⊢ t : T 
    ------------------------------- [∃-E]   -------------------------- [∃-I]   
    	    Γ ⊢ q                               Γ ⊢ ∃(x : T). p
    

Dans les règles [∀-I] et [∃-E], les conditions de typage Γ ⊢ Γ : Prop∗ et Γ ⊢ q : Prop servent aussi à exprimer que x doit être quelconque, au sens qu'il est possible de typer sans recourir à x. Une telle variable est dite "eigen" en allemand (propre, à la suite de Gentzen) et "fresh" en anglais (fraîche) : elle est propre à la quantification et sans usage par ailleurs. Voyons l'importance de ces conditions de typage sur un exemple.

Résultat faux mais preuve valide en l'absence de toute condition de typage

--------------------------------------
(x = 0), ∃(x : nat). (x = 0) ⊢ (x = 0)   
-------------------------------------------------- [∀-I] ?? 
(x = 0), ∃(x : nat). (x = 0) ⊢ ∀(x : nat). (x = 0)
  ∃(x : nat), (x = 0) ⊢ ∃(x : nat), (x = 0)
------------------------------------------- [∃-E]
∃(x : nat), (x = 0) ⊢ ∀(x : nat). (x = 0)

Avec les règles de typage, cette preuve est incorrecte dès l'application de la règle [∀-I].

4.5 Calcul des séquents

On s'intéresse à la seule version intuitionniste. La version classique ajoute des buts à droite du séquent.

  • [Id] : En supposant p, est déduit p si le séquent est bien typé.

    Γ ⊢ p : Prop  
    ------------ [Id]
      p, Γ ⊢ p
    
  • [∀-D] : ∀x. p est déduit si en supposant x quelconque, p est déduit, après substitution à x de t.
  • [∀-G] : ∀x. p et Γ est supposé s'il existe un terme t tel que p[x := t] et Γ est supposé.

    p[x := t], Γ ⊢ q   Γ ⊢ t : T         (x : T), Γ ⊢ p   Γ ⊢ Γ : Prop* 
    ---------------------------- [∀-G]   ------------------------------ [∀-D]
        ∀(x : T). p, Γ ⊢ q                      Γ ⊢ ∀(x : T). p
    
  • [∃-D] : ∃x, p est déduit s'il existe un terme t tel que p[x := t] est déduit.
  • [∃-G] : ∃x. p et Γ est supposé si pour un x quelconque, p et Γ est supposé.

    (x : T), p, Γ ⊢ q   Γ ⊢ q, Γ : Prop*        Γ ⊢ p[x := t]    Γ ⊢ t : T 
    ----------------------------------- [∃-G]   -------------------------- [∃-D]   
       ∃(x : T). p, Γ ⊢ q                             Γ ⊢ ∃(x : T). p
    

Author: Hervé Grall
Version history: v1: 2020-01-09; v2: 2020-01-20.
Comments or questions: Send a mail.
The webpage content is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.