Écriture d'une preuve

Publié le November 21, 2022
Tags: informatique, maths, preuve

En s’appuyant sur les notions abordées dans l’article sur l’intuition d’une preuve, cet article présente une formalisme d’écriture des preuves. Ici, on ne parle bien que d’écriture. Il n’est pas question ici de définir ce qui est vrai au sens “du monde” (ou mathématique). On ne présente ici que des “phrases” logiques, et les moyens dont on dispose de les organiser entre elles. L’adéquation de ces phrases avec le monde réelle sera abordé dans un prochain article.

Le processus mécanisé permettant d’arriver sur un fait étant a priori distinct d’une preuve au sens “du monde”, on utilisera le terme dérivable au lieu de vrai.

Le but de cet article est de présenter la façon générale dont peuvent être écrites les preuves. Il s’appuiera sur une logique particulière (dite LK ou Logique classique), mais il faut bien comprendre que ce ne sont que des exemples : en effet, il existe d’autres logiques que LK, mais le principe d’écriture des ces logiques reste celui décrit ici.

Les faits

Présentation générale

Pour rappel, les faits sont les assertions que l’on veut justifier par une preuve.

Faits possibles dans LK

Le précédent article présentait deux types de faits : les fait atomiques et les implications. Ces deux types se retrouvent dans la grammaire suivante.

A=|a|AA|AA|AAA = \bot \,|\, a \,|\, A \to A \,|\, A\wedge A \,|\, A \vee A

aa est un élément d’un ensemble 𝒜\mathcal{A} donné de symboles représentant l’ensemble des faits atomiques. Ces différents faits se lisent de la manière suivante

  • Le fait \bot est le fait faux
  • Le fait ABA\to B se lit AA implique BB
  • Le fait ABA\wedge B se lit AA et BB
  • Le fait ABA\vee B se lit AA ou BB

On pourra aussi utiliser le fait ABA \leftrightarrow B comme sucre syntaxique de (AB)(BA)(A\to B) \wedge (B \to A) et ¬A\neg A comme sucre syntaxique de AA \to \bot. On peut lire ces symboles de la manière suivante.

  • Le fait ABA \leftrightarrow B se lit AA équivaut à BB
  • Le fait ¬A\neg A se lit non AA

Exemples

A¬AA \vee \neg A Loi du tiers exclu. Ce fait est intuitivement vrai car elle affirme qu’un fait est toujours, soit vrai, soit faux.
¬(AB)¬A¬B\neg (A \wedge B) \leftrightarrow \neg A \vee\neg B Loi de De Morgan affirmant qu’il est possible de distribuer la négation autour de la conjonction.
¬(AB)¬A¬B\neg (A \vee B) \leftrightarrow \neg A\wedge\neg B Loi de De Morgan affirmant qu’il est possible de distribuer la négation autour de la disjonction.
¬¬AA\neg \neg A \leftrightarrow A Loi de la double négation affirmant que deux négations se suppriment.
(AB)CA(BC)(A \vee B)\vee C \leftrightarrow A\vee(B\vee C) Loi de l’associativité de la disjonction.
(AB)CA(BC)(A\wedge B) \wedge C \leftrightarrow A\wedge (B\wedge C) Loi de l’associativité de la conjonction.
ABBAA\wedge B \leftrightarrow B\wedge A Loi de la commutativité de la conjonction.
ABBAA\vee B \leftrightarrow B\vee A Loi de la commutativité de la disjonction.

Les preuves

Le précédent article a montré qu’une preuve était une composition de sous-preuves (prémisses). Les règles propres à la logique définissent les compositions autorisées par la logique. Schématiquement, une règle est de la forme

prémisse1prémissendéduction\frac{\text{prémisse}_1 \quad \cdots \quad \text{prémisse}_n}{\text{déduction}}

Au dénominateur se trouve ce qui peut être déduit (selon la règle de logique) des prémisses. On appelle ce dénominateur un sequent. les prémisses sont elles-mêmes d’autres preuves, ce qui donne à une preuve l’allure d’un arbre :

prémisse11déduction11prémisse1ndéduction1ndéduction1prémissen1déductionn1prémissenndéductionnndéductionndéduction\dfrac{\dfrac{\dfrac{\text{prémisse}_1^1}{\text{déduction}_1^1} \quad \cdots \quad \dfrac{\text{prémisse}^n_1}{\text{déduction}^n_1}}{\text{déduction}_1} \quad \cdots \quad \dfrac{\dfrac{\text{prémisse}^1_n}{\text{déduction}^1_n} \quad \cdots \quad \dfrac{\text{prémisse}_n^n}{\text{déduction}_n^n}}{\text{déduction}_n}}{\text{déduction}}

Séquents de LK

Il est rare de vouloir démontrer un fait dénué de toute hypothèse. C’est pourquoi, dans le cas général, on adjoint à chaque fait un ensemble d’hypothèses, noté Γ\Gamma ou Δ\Delta, qui est un ensemble de faits. Cet ensemble d’hypothèses est appelé environnement.

Un fait AA et l’environnement Γ\Gamma dans lequel il est défini est appelé un séquent et se note

ΓA\Gamma \vdash A

Ce séquent peut se lire “Étant donné un ensemble d’hypothèses Γ\Gamma, j’affirme le fait AA.

Règles logiques de LK

La logique LK, ou Logique classique, est la logique communément admise par tous. On y retrouve toutes les propriétés habituels en raisonnement logique : lois de De Morgan, associativité, commutativité et distributivité de la conjonction et de la disjonction, double négation, … On verra dans cet article une autre logique couramment utilisée, notamment en informatique.

La logique LK peut être définie à partir des règles suivantes. L’ensemble de ces règles exprime cette logique en utilisant le principe de la déduction naturelle. On montrera dans cet article qu’il existe d’autres moyens d’exprimer la même logique.

En déduction naturelle, les règles sont séparées en règles d’introduction et d’élimination pour chaque symbole possible dans les faits (\vee, \wedge, \to, \bot). Les premières font apparaître un symbole dans la conclusion de la règle, alors que les secondes le font appraître dans les prémisses. Dans la suite, les règles d’introduction se termine par un I\text{I} et les règles d’élimination par un E\text{E}.

ΓAΓAB(I)ΓBΓAB(I)ΓABΓ,ACΓ,BCΓC(E)\frac{\Gamma \vdash A}{\Gamma \vdash A \vee B}(\!\vee\text{I}) \quad \frac{\Gamma \vdash B}{\Gamma \vdash A \vee B}(\!\vee\text{I}) \quad \frac{\Gamma \vdash A \vee B \quad \Gamma, A\vdash C \quad \Gamma, B \vdash C}{\Gamma \vdash C}(\!\vee\text{E})

ΓAΓBΓAB(I)ΓABΓA(E)ΓABΓB(E)\frac{\Gamma \vdash A \quad \Gamma \vdash B}{\Gamma \vdash A \wedge B}(\!\wedge\text{I}) \quad \frac{\Gamma \vdash A \wedge B}{\Gamma \vdash A}(\!\wedge\text{E}) \quad \frac{\Gamma \vdash A \wedge B}{\Gamma \vdash B}(\!\wedge\text{E})

Γ,ABΓAB(I)ΓABΓAΓB(E)\frac{\Gamma, A \vdash B}{\Gamma \vdash A \to B}(\!\to\text{I}) \quad \frac{\Gamma \vdash A \to B \quad \Gamma \vdash A}{\Gamma \vdash B}(\!\to\text{E})

ΓAΓ¬AΓ(I)ΓΓA(E)\frac{\Gamma\vdash A \quad \Gamma\vdash \neg A}{\Gamma \vdash \bot}(\bot \text{I}) \quad \frac{\Gamma \vdash \bot}{\Gamma \vdash A}(\bot \text{E})

Par exemple, la règle (I)(\!\vee\text{I}) affirme que, dans cette logique, si je sais démontrer AA, alors je sais démontrer ABA\vee B.

Enfin, deux règles axiomatiques sont utilisées.

Γ,AA(Ax)ΓA¬A(TExcl)\frac{}{\Gamma, A \vdash A}(\text{Ax}) \quad \frac{}{\Gamma \vdash A \vee \neg A}(\text{TExcl})

La première désigne la preuve la plus simple : celle où le fait que l’on souhaite démontrer fait partie des hypothèses. La seconde est la règle du tiers exclu, qui affirme que n’importe quelle fait est soit vrai, soit faux.

Exemples

Dans cette section sont données des preuves de différents faits.

Lois de De Morgan

On rappelle l’une des lois de De Morgan

¬(AB)¬A¬B\neg (A \wedge B) \leftrightarrow \neg A \vee\neg B

Une preuve se déroule de la manière suivante

(1)(1) et (2)(2) sont des sous-preuves. La sous-preuve (1)(1) peut être donnée par l’arbre de preuve suivant

(11)(11) est une sous-preuve pouvant être donnée par l’arbre de preuve suivant

D’autre part, La sous-preuve (2)(2) peut être donnée par l’arbre de preuve suivant

(21)(21) et (22)(22) sont des sous-preuves. Par symétrie, la preuve (22)(22) peut être construite à partir de la preuve (21)(21) suivante

Double négation

On rappelle la loi de la double négation.

¬¬AA\neg \neg A \leftrightarrow A

Cette loi peut être dérivée par l’arbre de preuve suivant

(11)(11) est une sous-preuve pouvant être dérivée par l’arbre de preuve suivant

On notera l’utilisation de la règle du tiers exclu pour dériver la branche gauche de l’arbre. En fait, cette présence n’est pas un hasard car on peut montrer que la loi du tiers exclu est équivalente au sein de LK\TExcl\text{LK}\setminus \text{TExcl} à la loi de la double négation. Plus formellement, la notion d’équivalence est définie à partir de la notion d’admissibilité.

Considérant une logique \mathcal{L}, une règle RR est admissible dans \mathcal{L} lorsque l’ensemble des séquents dérivables dans {R}\mathcal{L} \cup \{R\} est le même que dans \mathcal{L}.

Deux règles R,SR, S sont équivalentes dans \mathcal{L} lorsque RR est admissible dans {S}\mathcal{L} \cup \{S\} et SS est admissible dans {R}\mathcal{L} \cup \{R\}.

Notons LJ=LK\TExcl\text{LJ} = \text{LK}\setminus \text{TExcl}, c’est à dire la logique obtenue à partir de LK\text{LK} privée de la loi du tiers exclu (TExcl\text{TExcl}), et posons la règle suivante

⪪AA(DNeg)\frac{}{\Gamma \vdash \neg \neg A \to A}(\text{DNeg})

Les règles DNeg et TExcl sont équivalentes dans LJ.

On a déjà montré que DNeg était admissible dans LJ{TExcl}\text{LJ} \cup \{\text{TExcl}\}. Réciproquement, voici une dérivation dutiers exclu.

(1)(1) est une sous-preuve pouvant être donnée par la dérivation suivante

et où (2)(2) est une sous-preuve pouvant être donnée par la dérivation suivante

L’équivalence de ces deux règles a abouti à l’établissement d’une nouvelle logique, LJ, nommée Logique intuitionniste.

Conclusion

Cet article a présenté un cadre formel et mécanique de représentation d’un raisonnement. Cette représentation n’est que syntaxique : en effet, on décrit ici l’enchaînement de règles de constructions, mais une étape est encore nécessaire pour comprendre ce que ces règles représentent. La recherche d’une sémantique d’une preuve est expliquée dans cet article.

La logique classique (LK) est souvent associée à l’intuition que l’on a de la logique, celle que l’on pratique tous les jours. Comme esquissé dans le paragraphe précédent, d’autres logiques sont possibles, ayant chacune des propriétés propres (logique intuitionniste, logique linéaire, …)