Règles d'inférence, dérivations¶

On présente ici la notion formelle de règle d'inférence et de dérivations. L'optique de ce chapitre étant de se placer dans un système déductif précis et contraint : la déduction naturelle, on pourra sauter ce paragraphe en première lecture.

On considère ici des données appelées jugements, il s'agit d'affirmations, on va voir dans la partie suivante le principal type de jugements qui vont nous intéresser : les séquents qui affirment qu'une formule est vraie sous certaines hypothèses.

Mais il ne s'agit que d'une facette des jugements que l'on peut rencontrer en informatique. On peut ainsi citer les jugements de types, qui affirment qu'un programme est d'un certain type.

Définition

On appelle règle d'inférence une règle qui relie des jugements, appelés prémisses, à un jugement appelé conclusion.

Il s'agit d'une formalisation abstraite d'une règle de déduction.

On la note à la manière d'un nœud dans un arbre en utilisant des formes génériques de jugements. Ainsi une règle d'inférence a la forme

Forme générale d'une règle d'inférence : prémisses au-dessus, conclusion au-dessous.

Une règle sans prémisse est appelée un axiome.

On donne parfois un nom symbolique à une règle pour pouvoir les distinguer plus facilement, il est alors indiqué à droite du trait.

Remarque

Ce qu'on signifie ici par le terme forme générique, c'est en fait, une forme de filtrage de motifs comme on le connait en OCaml : si les prémisses ont cette forme, voilà comment on construit la conclusion.

Exemple

On considère ici que les jugements sont des ensembles et on pose les règles suivantes :

Règles de construction d'ensembles : vide, singleton, union.

Les deux dernières règles sont génériques :

la règle singl fait référence à un élément $x$ quelconque, cela signifie qu'elle s'applique dès que le jugement contient un unique élément.
la seconde règle s'applique pour deux ensembles quelconques.

Définition

On dit qu'on peut dériver un jugement depuis un ensemble fixé de règles d'inférences, quand il est possible de réaliser un arbre fini dont les nœuds sont des applications des règles.

Un tel arbre est appelé une dérivation.

Remarque

Ici, il s'agit d'applications concrètes des règles et non plus de formes génériques.
Comme l'arbre est fini, ses feuilles sont nécessairement des règles axiomes.

Exemple

Dans le jeu de règles précédent, on peut dériver le jugement $\{1,2,3\}$ :

Un arbre de dérivation du jugement 1,2,3. — Un arbre de dérivation du jugement $\{1,2,3\}$.

On remarque qu'il existe ici de nombreuses dérivations de ce jugement. En fait, comme on peut le voir avec $\{1\} = \{1\} \cup \{1\}$, il est possible d'augmenter artificiellement l'arbre et donc l'ensemble de ces dérivations est infini.

On peut même prouver le résultat suivant : un ensemble est dérivable si et seulement si il est fini.

Remarque

On rajoute parfois des conditions sur les prémisses pour que la règle s'applique. Il ne s'agit pas d'une nouvelle prémisse, mais juste d'une restriction sur la construction de l'arbre. On peut rapprocher cela de la condition de garde dans un filtrage en OCaml (les when).

Par exemple, pour le jeu de règle sur l'union, on aurait pu demander à ce que l'union soit disjointe :

Règle d'union disjointe, avec sa condition (en violet).

Exemple

En remplaçant la règle $\cup$ par la règle $\sqcup$ et en enlevant la règle $\emptyset$, le nombre de dérivations d'un ensemble fini est fini : pour un ensemble non vide à $n$ éléments, c'est le nombre d'arbres binaires dont les feuilles sont étiquetées de manière bijective par les éléments de l'ensemble (l'ensemble vide n'est alors plus dérivable). On peut le calculer précisément avec les nombres de Catalan : il y a $C_{n-1} = \frac{1}{n}\binom{2n-2}{n-1}$ arbres binaires à $n$ feuilles, qu'on multiplie par $n!$ pour toutes les affectations possibles aux feuilles.

Déduction naturelle¶

Séquent, preuves¶

La déduction naturelle est un jeu de règles d'inférence associées à des jugements logiques : les séquents.

Définition

Étant donné un ensemble de formules logiques $F$, par exemple le calcul propositionnel, on appelle séquent pour $F$, un couple $(\Gamma,f)$ où $\Gamma \subset F$ et $f \in F$. On le note usuellement $\Gamma \vdash f$, le symbole $\vdash$ se lisant thèse ou donne.

Remarque

Un séquent est un jugement qui peut se lire sous la forme intuitive suivante : étant données les hypothèses $\Gamma$, je peux déduire $f$.

Définition

Dans le contexte des séquents, les dérivations sont appelées des preuves.

Quand on peut dériver le jugement $\vdash f$, on dit que $f$ est prouvable.

Système de règles pour le calcul propositionnel¶

Les règles de la déduction naturelle sont de trois types :

la règle axiome qui signifie que les jugements $\Delta \vdash f$ où $f \in \Delta$ sont prouvables :

Règle axiome.

On remarque qu'ici, on a fait le choix de le présenter simplement avec $, A$, cela ne signifie pas que $A$ est la dernière formule ou que $\Gamma$ soit non vide, mais juste que le contexte est de la forme $\Delta = \Gamma \cup \{ A \}$ ce qui est la forme générale d'un ensemble $\Delta$ tel que $A \in \Delta$.

les règles d'introduction qui font apparaître un symbole à la racine de l'arbre de la formule du séquent conclusion ;
les règles d'élimination qui font disparaître un symbole présent à la racine de l'arbre de la formule d'un des séquents prémisses.

Dans la suite, on étiquette par $i$ ou $e$ ces différents types de règles.

Remarque

Si on construit un arbre de preuve en partant de la conclusion, ce qui est le cas usuel, les règles d'introduction sont assez automatiques : il suffit de regarder le symbole à la racine de la formule à prouver pour en déduire la règle à appliquer. Toute la difficulté repose donc sur la bonne utilisation des règles d'élimination.

On peut aussi raisonner à l'envers en partant des axiomes.

Connecteur $\rightarrow$ :

Règles d'introduction et d'élimination de $\rightarrow$.

Dans la règle $\rightarrow_i$, l'hypothèse $A$ est déchargée : elle figure dans le contexte de la prémisse mais plus dans celui de la conclusion. La règle $\rightarrow_e$ est plus communément appelée le Modus Ponens dans le cadre de l'étude des raisonnements en philosophie. C'est celle qui permet d'utiliser un résultat intermédiaire $A$, du moment qu'il est prouvable, pour raisonner. C'est la principale manière de faire apparaître des hypothèses intermédiaires quand elles ne sont pas directement dans le contexte.
Connecteur $\wedge$ :

Règles d'introduction et d'élimination de $\wedge$.

Ici, il y a deux règles d'élimination, une règle gauche et une règle droite, qui indiquent la partie de la conjonction conservée dans le séquent conclusion.
Connecteur $\vee$ :

Règles d'introduction et d'élimination de $\vee$.

Ici, la règle d'introduction est latéralisée car elle correspond au côté de la disjonction que l'on prouve. Attention il y a une perte d'information ici et ce n'est pas toujours une bonne idée de faire cette règle sans avoir une bonne raison de choisir la gauche ou la droite.

La règle d'élimination est plus communément appelée une disjonction de cas en mathématiques. Ici, il faut s'assurer que la formule sur laquelle s'effectue la disjonction est prouvable puis faire la preuve dans chacun des deux cas, les hypothèses $A$ et $B$ étant déchargées.
Connecteur $\neg$ :

Règles pour $\neg$ et élimination de $\bot$.

La règle d'introduction de la négation revient en fait à considérer que $\neg A = A \rightarrow \bot$ : c'est une règle $\rightarrow_i$ déguisée, où l'hypothèse $A$ est déchargée. La règle d'élimination de la négation est souvent confondue avec le raisonnement par l'absurde. Il s'agit juste de montrer une formule et sa négation pour en déduire une contradiction.

La règle d'élimination de l'absurde $\bot_e$ (ex falso quodlibet) permet de déduire n'importe quelle formule $C$ d'une contradiction : c'est elle qui permet d'exploiter une contradiction obtenue par $\neg_e$.

Attention, le raisonnement par l'absurde proprement dit, qui consiste à déduire $\Gamma \vdash A$ de $\Gamma, \neg A \vdash \bot$, n'est pas une règle de ce système : avec les règles ci-dessus, on obtient seulement $\Gamma \vdash \neg \neg A$ par $\neg_i$. On verra qu'il faut pour cela se placer en logique classique.

Exemple

Voici une preuve de $(A \vee B) \wedge C \vdash (A \wedge C) \vee (B \wedge C)$ :

Preuve de (A vee B) wedge C vdash (A wedge C) vee (B wedge C) ; conclusion en vert. — Preuve de $(A \vee B) \wedge C \vdash (A \wedge C) \vee (B \wedge C)$ ; conclusion en vert.

Le théorème suivant affirme la correction de la déduction naturelle : elle ne prouve rien qui ne soit pas une conséquence logique. Ici, pour $\Gamma$ éventuellement infini, on note $\Gamma \models f$ lorsque toute valuation rendant vraies toutes les formules de $\Gamma$ rend vraie $f$ (pour $\Gamma$ fini, cela coïncide avec la définition du chapitre sur le calcul propositionnel).

Théorème

Soit $Prop$ l'ensemble des formules du calcul propositionnel et $\Gamma \subset Prop$, $f \in Prop$.

Si $\Gamma \vdash f$ est prouvable alors $\Gamma \models f$.

Preuve

On montre par induction structurelle sur la preuve que tout séquent prouvable $\Delta \vdash \varphi$ vérifie $\Delta \models \varphi$. L'hypothèse d'induction porte donc sur les séquents prémisses, dont le contexte peut différer de celui de la conclusion (règles $\rightarrow_i$, $\vee_e$, $\neg_i$).

Dans chaque cas, on note $\Gamma$ le contexte du séquent conclusion et on considère une valuation $v$ telle que pour tout $f \in \Gamma$, $[f]_v = V$.

Si la preuve est réduite à un axiome $\Gamma, A \vdash A$, alors comme $A$ est dans le contexte, $[A]_v = V$. Ainsi $\Gamma, A \models A$.
Si la preuve est obtenue par une règle $\rightarrow_i$ à partir de $\Gamma, A \vdash B$, on raisonne sur $[A]_v$ :

Si $[A]_v = V$, alors $v$ rend vraies toutes les formules de $\Gamma \cup \{A\}$ et comme, par hypothèse d'induction, $\Gamma, A \models B$, on a forcément $[B]_v = V$ et ainsi $[A \rightarrow B]_v = V$.

Si $[A]_v = F$, alors trivialement $[A \rightarrow B]_v = V$.

Dans tous les cas, on a bien $[A \rightarrow B]_v = V$, ainsi $\Gamma \models A \rightarrow B$.
Si la preuve est obtenue par une règle $\rightarrow_e$, comme $\Gamma \vdash A \rightarrow B$ et $\Gamma \vdash A$ sont prouvables, par hypothèses d'induction on a $[A \rightarrow B]_v = [A]_v = V$ et cela force $[B]_v = V$ selon la table de vérité de l'implication. Ainsi $\Gamma \models B$.
Si la preuve est obtenue par une règle $\wedge_i$, de $\Gamma \vdash A$ et $\Gamma \vdash B$ prouvables, on peut en déduire par hypothèse d'induction que $[A]_v = [B]_v = V$, et donc en vertu de la table de vérité de $\wedge$, on a $[A \wedge B]_v = V$. Donc, $\Gamma \models A \wedge B$.
Si la preuve est obtenue par une règle $\wedge_{e,g}$ ou $\wedge_{e,d}$, on a $\Gamma \vdash A \wedge B$ prouvable donc par hypothèse d'induction $[A \wedge B]_v = V$ ; le seul cas de la table de vérité est celui où $[A]_v = [B]_v = V$ et donc $\Gamma \models A$ ainsi que $\Gamma \models B$.
Pour $\vee_{i,g}$ (resp. $\vee_{i,d}$), $[A]_v = V$ (resp. $[B]_v = V$) entraîne $[A \vee B]_v = V$.
Pour $\vee_e$, par hypothèse d'induction $[A \vee B]_v = V$, donc $[A]_v = V$ ou $[B]_v = V$. Dans le premier cas, $v$ rend vraies les formules de $\Gamma \cup \{A\}$ et $\Gamma, A \models C$ donne $[C]_v = V$ ; le second cas est symétrique.
Pour $\neg_i$, si on avait $[A]_v = V$, l'hypothèse d'induction $\Gamma, A \models \bot$ donnerait $[\bot]_v = V$, ce qui est impossible. Donc $[A]_v = F$ et $[\neg A]_v = V$.
Pour $\neg_e$ et $\bot_e$, les hypothèses d'induction donneraient $[A]_v = [\neg A]_v = V$ (resp. $[\bot]_v = V$), ce qui est impossible : il n'existe donc aucune valuation $v$ rendant vraies les formules de $\Gamma$, et $\Gamma \models \varphi$ pour toute formule $\varphi$.

Corollaire

Les formules prouvables sont des tautologies.

Logique classique¶

Certaines formules dont on sait qu'elles sont des tautologies du calcul propositionnel ne semblent pas prouvables.

La formule la plus emblématique dans ce cas est le tiers exclu : $\vdash A \vee \neg A$ n'est pas prouvable.

Remarque

Comment montrer qu'une formule n'est pas prouvable ?

Ce n'est pas une question facile à traiter directement, car cela nécessite de raisonner sur l'ensemble des arbres de preuve. La manière usuelle de le montrer est de le faire de manière indirecte :

on construit un modèle de la déduction, c'est-à-dire une sémantique qui vérifie les règles. Dans la partie précédente, on a construit un modèle booléen en liant la prouvabilité à la conséquence logique.
on montre que la formule n'est pas vraie dans ce modèle (attention, sur des modèles non booléens, cela ne signifie pas qu'elle est fausse).
si la formule était prouvable, la correction du modèle entraînerait que la formule serait vraie.
donc, la formule n'est pas prouvable.

Pour le tiers exclu, il faut utiliser un modèle non booléen, par exemple une sémantique à trois valeurs de vérité comme celle de Gödel : c'est l'objet de la partie bonus Sémantique de Gödel.

On parle de déduction naturelle classique quand on ajoute la règle axiome suivante (tiers exclu) :

Sans cette règle, on parle de déduction naturelle intuitionniste. Les formules prouvées dans ce cadre sont encore des tautologies : la preuve de correction s'étend directement, car $A \vee \neg A$ est une tautologie.

Remarque

L'usage usuel de cette règle est de la combiner avec une disjonction par cas :

Tiers exclu combiné à une disjonction par cas.

Remarque

En logique classique, le raisonnement par l'absurde devient une règle dérivée : si $\Gamma, \neg A \vdash \bot$ est prouvable, on obtient $\Gamma, \neg A \vdash A$ par $\bot_e$, et $\Gamma, A \vdash A$ est un axiome ; la disjonction de cas sur $A \vee \neg A$ ci-dessus donne alors $\Gamma \vdash A$. Réciproquement, on peut montrer qu'en ajoutant la règle du raisonnement par l'absurde (ou l'élimination de la double négation $\neg \neg A \vdash A$) au système intuitionniste, on peut prouver le tiers exclu.

On peut alors démontrer le théorème suivant auquel on fait référence sous le terme de complétude :

Théorème

Soit $Prop$ l'ensemble des formules du calcul propositionnel et $\Gamma \subset Prop$, $f \in Prop$.

Si $\Gamma \models f$ alors le séquent $\Gamma \vdash f$ est prouvable en déduction naturelle classique.

La preuve de ce théorème est hors de portée de ce cours. Ce théorème est faux pour la déduction naturelle intuitionniste, puisque le tiers exclu est une tautologie qui n'y est pas prouvable.

Règles pour la logique du premier ordre¶

On considère ici $F$ les formules de la logique du premier ordre.

Variables libres¶

Si $f \in F$, on dit qu'une variable est libre dans $f$ quand elle a au moins une occurrence dans $f$ qui n'est pas liée à un quantificateur. On note $FV(f)$ les variables libres de $f$.

Exemple

Dans $f \equiv y = x \wedge \forall x. \exists z. x < z$, les variables $x$ et $y$ sont libres, la variable $x$ est aussi liée à droite dans la formule, mais elle est libre si au moins une de ses occurrences est libre.

On a donc $FV(f) = \{ x, y\}$.

Remarque

On utilise ici la notation $FV$ pour free variables afin d'éviter l'ambiguïté d'un $VL$ pouvant faire référence également aux variables liées.

$\alpha$-équivalence¶

Si on considère une formule $\forall x. P$ et que l'on note $P'$ la formule obtenue en changeant toutes les occurrences libres de $x$ dans $P$ par la variable $y$ supposée non libre dans $P$ (et telle qu'aucune occurrence libre de $x$ dans $P$ ne se trouve sous un quantificateur liant $y$, sinon $y$ serait capturée), on dit que la formule $\forall y. P'$ est $\alpha$-équivalente à $\forall x.P$. On étend cela naturellement au quantificateur $\exists$ ainsi qu'à des quantificateurs à profondeur quelconque. On pourra noter $f \equiv_\alpha g$ pour dire que $f$ et $g$ sont $\alpha$-équivalentes.

Bien définir cette équivalence est délicat, on passe outre toute difficulté ici.

Exemple

$\forall x. P(x,y) \rightarrow \exists y. R(y,x) \equiv_\alpha \forall t. P(t,y) \rightarrow \exists z. R(z,t)$

Ici, la première occurrence de $y$ est libre et ne peut changer par $\alpha$-équivalence.

Remarque

On connaît déjà cette notion dans deux contextes :

en mathématiques quand on change la variable d'intégration
en informatique quand on renomme les variables

On considère ici que les règles s'appliquent modulo $\alpha$-équivalence. Ainsi l'application suivante est bien un axiome :

Un axiome modulo alpha-équivalence. — Un axiome modulo $\alpha$-équivalence.

Substitution¶

Soit $f$ une formule, $x$ une variable et $t$ un terme, on note $f[x\backslash t]$ la formule obtenue en remplaçant chaque occurrence libre de $x$ dans $f$ par $t$, après avoir renommé (par $\alpha$-équivalence) les variables liées de $f$ qui sont libres dans $t$ : ainsi aucune variable de $t$ n'est capturée par un quantificateur de $f$.

Exemple

Si $f \equiv \forall x. P(x, y) \rightarrow P(x, z)$ et $g$ est un symbole de fonction, alors $f[y \backslash g(x, z)] = \forall x'. P(x', g(x, z)) \rightarrow P(x',z)$ : on a d'abord renommé la variable liée $x$ en $x'$, sinon l'occurrence libre de $x$ dans $g(x,z)$ aurait été capturée par le quantificateur $\forall x$.

On remarque que $f[x \backslash t] = f$ car toutes les occurrences de $x$ sont liées.

Règles pour $\forall, \exists$¶

On conserve les règles précédentes et on ajoute les règles suivantes pour les quantificateurs.

Règles pour $\forall$ :

Règles pour $\forall$ ; la condition sur les variables libres est en violet.

Pour bien comprendre ces règles, il est nécessaire de les rapprocher de l'usage qu'on en fait en mathématiques. La règle d'introduction correspond au moment où on introduit une variable dans une preuve en écrivant Soit $x$.... La condition de non présence de $x$ comme variable libre dans le contexte est très importante. Sinon, on pourrait prouver que tous les nombres sont irrationnels en commençant par Soit $\pi$ et en utilisant le fait que $\pi$ est irrationnel. Quand on introduit un nom avec Soit en mathématiques, on veut le faire en toute généralité.

La règle d'élimination est au contraire une règle de spécialisation : si on sait démontrer un résultat pour tous les $x$, on sait en déduire le résultat dans le cas d'un $x$ particulier, remplacé par un terme $t$ quelconque.

Règles pour $\exists$ :

Règles pour $\exists$ ; la condition sur les variables libres est en violet.

La règle d'introduction correspond en mathématiques au fait de donner un témoin d'existence d'une propriété. Ici, on affirme que c'est $x = t$ qui fonctionne.

La règle d'élimination correspond au raisonnement Soit $x$ tel que $A$ : sachant qu'il existe un $x$ vérifiant $A$, on introduit un tel $x$ et l'hypothèse $A$ (qui possède $x$ comme variable libre) pour prouver $B$. L'hypothèse $A$ est alors déchargée. La condition $x \not\in FV(\Gamma, B)$ assure que $x$ est un nom nouveau, sur lequel on ne sait rien d'autre que $A$, et qu'il n'apparaît pas dans la conclusion.

Remarque

Les quantificateurs rendent complexe l'application des règles. Il faut s'assurer que ce que l'on écrit a un sens mathématique.

Règles hypothèses¶

Attention on ne peut pas utiliser ces règles au concours sans démontrer qu'elles fonctionnent avant.

On peut rajouter des méta-règles, c'est-à-dire des configurations pour lesquelles, quitte à appliquer une succession de règles, on peut passer d'un séquent conclusion à des séquents prémisses.

On a ainsi pu voir une telle méta-règle avec la disjonction sur le tiers exclu, on pourrait ainsi la noter :

Méta-règle de disjonction sur le tiers exclu.

Le cas usuel de règles intéressantes sont les règles hypothèses qui permettent de raisonner directement sur les hypothèses :

Méta-règle hypothèse pour wedge. — Méta-règle hypothèse pour $\wedge$.

Utilisation d'un assistant de preuve (Bonus)¶

Construire un arbre de preuve à la main est fastidieux et il est facile d'y glisser une erreur, notamment sur les contextes. Un assistant de preuve est un logiciel qui construit l'arbre avec nous et vérifie que chaque règle est correctement appliquée. L'assistant dedunat mentionné dans les exercices suit exactement les règles de ce chapitre. Les assistants utilisés en recherche et dans l'industrie, comme Rocq (anciennement Coq, développé en France) ou Lean, reposent sur les mêmes principes.

On y travaille comme on l'a conseillé plus haut : en partant de la conclusion. On énonce le séquent à prouver, appelé le but, puis on applique des tactiques qui remplacent le but par les prémisses d'une règle. L'assistant affiche à chaque étape le contexte et le ou les buts restants. La preuve est terminée quand il n'y a plus de but.

Exemple

Voici en Rocq la preuve de $(A \vee B) \wedge C \vdash (A \wedge C) \vee (B \wedge C)$ donnée en exemple plus haut, présentée ici sous la forme $\vdash (A \vee B) \wedge C \rightarrow (A \wedge C) \vee (B \wedge C)$. En commentaire, on indique la règle correspondante.

Theorem distrib (A B C : Prop) : (A \/ B) /\ C -> (A /\ C) \/ (B /\ C).
Proof.
  intro H.                    (* ->i : H : (A \/ B) /\ C dans le contexte *)
  destruct H as [HAB HC].     (* /\e,g et /\e,d sur l'hypothèse H *)
  destruct HAB as [HA | HB].  (* \/e : deux buts, avec HA : A puis HB : B *)
  - left.                     (* \/i,g *)
    split.                    (* /\i : deux buts A et C *)
    + exact HA.               (* ax *)
    + exact HC.               (* ax *)
  - right.                    (* \/i,d *)
    split.                    (* /\i *)
    + exact HB.               (* ax *)
    + exact HC.               (* ax *)
Qed.

Les puces - et + correspondent aux branches de l'arbre de preuve.

Le tableau suivant donne la correspondance entre les tactiques de base de Rocq et les règles de la déduction naturelle.

Tactique	Règle
`exact H` ou `assumption`	$ax$
`intro H`	$\rightarrow_i$, et aussi $\neg_i$ car $\neg A$ est défini comme $A \rightarrow \bot$
`apply H` avec `H : A -> B`	$\rightarrow_e$ : le but $B$ est remplacé par $A$
`split`	$\wedge_i$
`destruct H as [H1 H2]` avec `H : A /\ B`	$\wedge_{e,g}$ et $\wedge_{e,d}$
`left`, `right`	$\vee_{i,g}$, $\vee_{i,d}$
`destruct H as [H1 \| H2]` avec `H : A \/ B`	$\vee_e$
`exfalso`	$\bot_e$
`intro x` sur un but $\forall x. A$	$\forall_i$
`exists t`	$\exists_i$

Remarque

Les tactiques destruct agissent sur une hypothèse du contexte plutôt que sur le but : ce sont les règles hypothèses vues plus haut.
Rocq est intuitionniste par défaut : le tiers exclu n'est pas prouvable sans l'ajouter explicitement comme axiome (par exemple avec Require Import Classical., qui fournit classic : forall P, P \/ ~ P).
En fait, Rocq ne stocke pas l'arbre mais un programme : la commande Show Proof. affiche un terme fonctionnel qui ressemble beaucoup à du OCaml, avec un fun pour intro et un match pour chaque destruct. C'est la correspondance de Curry-Howard présentée dans le chapitre Introduction au lambda-calcul.

Sémantique de Gödel (Bonus)¶

On a vu que le tiers exclu $A \vee \neg A$ est une tautologie mais qu'il n'est pas prouvable en déduction naturelle intuitionniste. Pour le démontrer, on suit la méthode de la remarque Comment montrer qu'une formule n'est pas prouvable ? : on construit un modèle à trois valeurs de vérité, dû à Gödel (1932), dans lequel toutes les formules prouvables sont vraies mais pas le tiers exclu.

L'idée est d'ajouter aux valeurs $0$ (faux) et $1$ (vrai) une valeur intermédiaire $\frac{1}{2}$, qu'on peut lire comme « pas encore démontré ».

Définition

On pose $\mathbb{G} = \{0, \frac{1}{2}, 1\}$ muni de l'ordre usuel. Une valuation de Gödel est une application $v$ des variables propositionnelles dans $\mathbb{G}$. On l'étend aux formules par :

$[\bot]_v = 0$ ;
$[A \wedge B]_v = \min([A]_v, [B]_v)$ et $[A \vee B]_v = \max([A]_v, [B]_v)$ ;
$[A \rightarrow B]_v = 1$ si $[A]_v \le [B]_v$ et $[A \rightarrow B]_v = [B]_v$ sinon ;
$[\neg A]_v = [A \rightarrow \bot]_v$, c'est-à-dire $1$ si $[A]_v = 0$ et $0$ sinon.

Pour un ensemble de formules $\Gamma$, on pose $[\Gamma]_v = \min \enscomp{[f]_v}{f \in \Gamma}$, avec la convention $[\emptyset]_v = 1$ (ce minimum existe car $\mathbb{G}$ est fini).

Remarque

Restreinte à $\{0, 1\}$, cette sémantique coïncide avec les tables de vérité usuelles. Une formule qui vaut $1$ pour toute valuation de Gödel est donc en particulier une tautologie.

Exemple

Pour $[A]_v = \frac{1}{2}$, on a $[\neg A]_v = 0$ et donc $[A \vee \neg A]_v = \max(\frac{1}{2}, 0) = \frac{1}{2} \neq 1$.

De même $[\neg \neg A]_v = 1$ et ainsi $[\neg \neg A \rightarrow A]_v = \frac{1}{2}$.

La propriété clé de l'implication est la suivante, à rapprocher des règles $\rightarrow_i$ et $\rightarrow_e$.

Lemme

Pour tous $a, b, c \in \mathbb{G}$, en notant $a \Rightarrow b$ la valeur de l'implication, on a

\[ c \le (a \Rightarrow b) \iff \min(c, a) \le b \]

Preuve

Si $a \le b$, alors $a \Rightarrow b = 1$ donc l'inégalité de gauche est vraie, et $\min(c,a) \le a \le b$ donc celle de droite aussi.
Si $a > b$, alors $a \Rightarrow b = b$. Si $c \le b$, alors $\min(c, a) \le c \le b$. Réciproquement, si $\min(c,a) \le b$, comme $a > b$, ce minimum ne peut pas être $a$, c'est donc $c$ et $c \le b$.

Théorème

Si $\Gamma \vdash f$ est prouvable en déduction naturelle intuitionniste, alors pour toute valuation de Gödel $v$, $[\Gamma]_v \le [f]_v$.

En particulier, si $f$ est prouvable, alors $[f]_v = 1$ pour toute valuation de Gödel $v$.

Preuve

Comme pour la correction booléenne, on procède par induction sur la preuve. On fixe $v$, on note $\Gamma$ le contexte de la conclusion, $c = [\Gamma]_v$ et on note simplement $a = [A]_v$, $b = [B]_v$, $d = [C]_v$. On remarque que $[\Gamma, A]_v = \min(c, a)$.

Axiome : $\min(c, a) \le a$.
$\rightarrow_i$ : l'hypothèse d'induction donne $\min(c, a) \le b$, donc $c \le (a \Rightarrow b)$ par le lemme.
$\rightarrow_e$ : on a $c \le (a \Rightarrow b)$ et $c \le a$. Par le lemme, $\min(c, a) \le b$ et comme $\min(c, a) = c$, $c \le b$.
$\wedge_i$, $\wedge_{e,g}$, $\wedge_{e,d}$ : $c \le a$ et $c \le b$ équivaut à $c \le \min(a, b)$.
$\vee_{i,g}$, $\vee_{i,d}$ : si $c \le a$ ou $c \le b$, alors $c \le \max(a, b)$.
$\vee_e$ : on a $c \le \max(a, b)$, $\min(c, a) \le d$ et $\min(c, b) \le d$. Si $a \ge b$, alors $c \le a$ donc $c = \min(c, a) \le d$. Sinon $c \le b$ et $c = \min(c, b) \le d$.
$\neg_i$ et $\neg_e$ : ce sont les cas $\rightarrow_i$ et $\rightarrow_e$ avec $B = \bot$, puisque $[\neg A]_v = [A \rightarrow \bot]_v$.
$\bot_e$ : on a $c \le [\bot]_v = 0$ donc $c = 0 \le d$.

Corollaire

Les formules $A \vee \neg A$, $\neg \neg A \rightarrow A$ et $((A \rightarrow B) \rightarrow A) \rightarrow A$ (loi de Peirce) ne sont pas prouvables en déduction naturelle intuitionniste.

Preuve

D'après le théorème, il suffit de trouver une valuation de Gödel qui ne donne pas la valeur $1$ à ces formules. L'exemple précédent traite les deux premières avec $[A]_v = \frac{1}{2}$. Pour la loi de Peirce, avec $[A]_v = \frac{1}{2}$ et $[B]_v = 0$, on a $[A \rightarrow B]_v = 0$, puis $[(A \rightarrow B) \rightarrow A]_v = 1$ et enfin $[((A \rightarrow B) \rightarrow A) \rightarrow A]_v = \frac{1}{2}$.

Remarque

Ce modèle n'est pas complet pour la logique intuitionniste : certaines formules valent toujours $1$ sans être prouvables, par exemple $(A \rightarrow B) \vee (B \rightarrow A)$. Il sert uniquement à montrer que des formules ne sont pas prouvables.
On peut obtenir des modèles complets de la logique intuitionniste en remplaçant $\mathbb{G}$ par des structures plus riches (algèbres de Heyting, modèles de Kripke), ce qui dépasse le cadre de ce cours.
Ce résultat ne doit pas être confondu avec le théorème de complétude de Gödel (1929), qui affirme que toute formule du premier ordre vraie dans tous les modèles est prouvable en logique classique : c'est l'analogue au premier ordre du théorème de complétude énoncé plus haut.

Lambda-calcul simplement typé (Bonus)¶

Cette partie a été déplacée dans son propre chapitre Introduction au lambda-calcul.

Exercices¶

Pour réaliser les preuves, vous pouvez utiliser l'assistant de preuve dédié au programme dedunat.

Exercice

Démontrer en déduction naturelle :

$(A \rightarrow B) \wedge (B \rightarrow C) \rightarrow A \rightarrow C$
$A \wedge B \rightarrow B \wedge A$
$(A \vee B \rightarrow C) \rightarrow A \rightarrow C$
$A \vee (A \wedge B) \rightarrow A$
$\neg (A \vee B) \rightarrow \neg A \wedge \neg B$
$\neg A \vee \neg B \rightarrow \neg (A \wedge B)$
$\neg A \wedge \neg B \rightarrow \neg (A \vee B)$
$(A \rightarrow (B \rightarrow (C \rightarrow D))) \rightarrow (B \rightarrow C \wedge A \rightarrow D)$
$(\neg A \vee B) \rightarrow (A \rightarrow B)$
$A \rightarrow \neg \neg A$

Réponse

1.

2.

3.

4.

5.

6.

7.

8.

9.

10.

Exercice

On suppose ici la règle classique du tiers exclu.

Démontrez :

a) $\neg \neg A \rightarrow A$
b) $(A \rightarrow B) \rightarrow \neg A \vee B$
c) $\neg (A \wedge B) \rightarrow \neg A \vee \neg B$
d) $((A \rightarrow B) \rightarrow A) \rightarrow A$ (loi de Peirce)

Réponse

a.

b.

c.

d.

Exercice

Démontrez en déduction naturelle :

a) $(\forall x.P(x)) \rightarrow \exists x.P(x)$
b) $\exists x. \forall y. P(x,y) \rightarrow \forall y. \exists x. P(x,y)$
c) $P(a) \rightarrow Q(a) \rightarrow \exists x. P(x) \wedge Q(x)$
d) $(\forall x.P(x) \rightarrow Q(x)) \rightarrow P(a) \rightarrow Q(a)$
e) $(\forall x. P(x) \rightarrow Q(x)) \rightarrow (\forall x. Q(x) \rightarrow R(x)) \rightarrow (\forall x. P(x) \rightarrow R(x))$

Réponse

J'ai fait le choix ici d'utiliser des nouveaux noms, comme $x_0$, pour bien marquer l'application des règles. Techniquement, on peut tout faire en utilisant les mêmes noms de variables que ceux qui sont quantifiés.

a.

b.

c.

d.

e.

Exercice

On parle de méta-règle

Quand étant donné des preuves de $P_1, \dots, P_n$, on peut toujours appliquer des règles pour démontrer $C$.

C'est une sorte de sucre syntaxique qui permet des raccourcis de raisonnement.

Démontrez les méta-règles hypothèses du formulaire.

Réponse

Hypothèse $\wedge$ :

Justification de la méta-règle hypothèse wedge par les règles usuelles. — Justification de la méta-règle hypothèse $\wedge$ par les règles usuelles.

La règle struct utilisée ici est l'affaiblissement : si $\Gamma \vdash C$ est prouvable, alors $\Gamma, D \vdash C$ l'est aussi. Ce n'est pas une règle du système, mais elle se démontre par induction sur la preuve (en ajoutant $D$ à tous les contextes, quitte à renommer les variables liées par $\forall_i$ ou $\exists_e$ pour respecter les conditions sur les variables libres).

Tactique	Règle
`exact H` ou `assumption`	\(ax\)
`intro H`	\(\rightarrow_i\), et aussi \(\neg_i\) car \(\neg A\) est défini comme \(A \rightarrow \bot\)
`apply H` avec `H : A -> B`	\(\rightarrow_e\) : le but \(B\) est remplacé par \(A\)
`split`	\(\wedge_i\)
`destruct H as [H1 H2]` avec `H : A /\ B`	\(\wedge_{e,g}\) et \(\wedge_{e,d}\)
`left`, `right`	\(\vee_{i,g}\), \(\vee_{i,d}\)
`destruct H as [H1 \| H2]` avec `H : A \/ B`	\(\vee_e\)
`exfalso`	\(\bot_e\)
`intro x` sur un but \(\forall x. A\)	\(\forall_i\)
`exists t`	\(\exists_i\)

Règles d'inférence, dérivations¶

Déduction naturelle¶

Séquent, preuves¶

Système de règles pour le calcul propositionnel¶

Logique classique¶

Règles pour la logique du premier ordre¶

Variables libres¶

\(\alpha\)-équivalence¶

Substitution¶

Règles pour \(\forall, \exists\)¶

Règles hypothèses¶

Utilisation d'un assistant de preuve (Bonus)¶

Sémantique de Gödel (Bonus)¶

Lambda-calcul simplement typé (Bonus)¶

Exercices¶