07. Systèmes de Preuves

Qu’est-ce qu’une preuve formelle?

Une preuve formelle est une dérivation syntaxique qui établit qu’une formule est un théorème d’un système logique. Contrairement aux preuves informelles en mathématiques, chaque étape est justifiée par une règle explicite.

Motivation

Pourquoi formaliser les preuves?

1. Vérification mécanique: Une preuve formelle peut être vérifiée par un algorithme.
2. Rigueur absolue: Aucune étape n’est “évidente” — tout est explicite.
3. Fondations: Permet d’étudier les limites du raisonnement (Gödel).
4. Applications: Assistants de preuve (Coq, Lean), vérification de logiciels.

Systèmes de preuves

Il existe plusieurs styles de systèmes de preuves:

Ce cours se concentre sur la déduction naturelle, développée par Gentzen (1934-35), qui reflète le raisonnement mathématique naturel.

Déduction naturelle propositionnelle

Principe

En déduction naturelle, chaque connecteur a:

• Des règles d’introduction pour établir une formule avec ce connecteur.
• Des règles d’élimination pour utiliser une formule avec ce connecteur.

Notation

Un jugement a la forme:

$$ \Gamma \vdash \varphi $$

signifiant “$\varphi$ est dérivable à partir des hypothèses $\Gamma$”.

Les règles sont présentées sous forme de fractions:

$$ \frac{\text{prémisses}}{\text{conclusion}} ; \text{(nom)} $$

Règles pour la conjonction ($\land$)

Introduction de $\land$

$$ \frac{\Gamma \vdash \varphi \quad \Gamma \vdash \psi}{\Gamma \vdash \varphi \land \psi} ; (\land I) $$

Pour prouver une conjonction, prouver les deux conjoints.

Élimination de $\land$

$$ \frac{\Gamma \vdash \varphi \land \psi}{\Gamma \vdash \varphi} ; (\land E_1) \qquad \frac{\Gamma \vdash \varphi \land \psi}{\Gamma \vdash \psi} ; (\land E_2) $$

D’une conjonction, on peut extraire chaque conjoint.

Règles pour la disjonction ($\lor$)

Introduction de $\lor$

$$ \frac{\Gamma \vdash \varphi}{\Gamma \vdash \varphi \lor \psi} ; (\lor I_1) \qquad \frac{\Gamma \vdash \psi}{\Gamma \vdash \varphi \lor \psi} ; (\lor I_2) $$

Élimination de $\lor$ (Analyse par cas)

$$ \frac{\Gamma \vdash \varphi \lor \psi \quad \Gamma, \varphi \vdash \chi \quad \Gamma, \psi \vdash \chi}{\Gamma \vdash \chi} ; (\lor E) $$

Si on a $\varphi \lor \psi$ et qu’on peut prouver $\chi$ dans chaque cas, alors $\chi$.

Règles pour l’implication ($\rightarrow$)

Introduction de $\rightarrow$ (Déduction)

$$ \frac{\Gamma, \varphi \vdash \psi}{\Gamma \vdash \varphi \rightarrow \psi} ; (\rightarrow I) $$

Pour prouver $\varphi \rightarrow \psi$, supposer $\varphi$ et en déduire $\psi$.

Élimination de $\rightarrow$ (Modus Ponens)

$$ \frac{\Gamma \vdash \varphi \rightarrow \psi \quad \Gamma \vdash \varphi}{\Gamma \vdash \psi} ; (\rightarrow E) $$

De $\varphi \rightarrow \psi$ et $\varphi$, on déduit $\psi$.

Règles pour la négation ($\neg$)

Introduction de $\neg$ (Réduction à l’absurde)

$$ \frac{\Gamma, \varphi \vdash \bot}{\Gamma \vdash \neg\varphi} ; (\neg I) $$

Pour prouver $\neg\varphi$, supposer $\varphi$ et dériver une contradiction.

Élimination de $\neg$

$$ \frac{\Gamma \vdash \varphi \quad \Gamma \vdash \neg\varphi}{\Gamma \vdash \bot} ; (\neg E) $$

De $\varphi$ et $\neg\varphi$, on déduit l’absurde.

Élimination de $\bot$ (Ex falso)

$$ \frac{\Gamma \vdash \bot}{\Gamma \vdash \varphi} ; (\bot E) $$

De l’absurde, on peut déduire n’importe quoi.

Règle classique: Double négation

$$ \frac{\Gamma \vdash \neg\neg\varphi}{\Gamma \vdash \varphi} ; (DN) $$

Cette règle distingue la logique classique de la logique intuitionniste.

Alternativement, on peut utiliser le tiers exclu:

$$ \frac{}{\Gamma \vdash \varphi \lor \neg\varphi} ; (EM) $$

Exemple de preuve: $p \rightarrow q, q \rightarrow r \vdash p \rightarrow r$

Prouvons la transitivité de l’implication:

$$ \begin{array}{lll}

1. & p \rightarrow q & \text{hypothèse} \
2. & q \rightarrow r & \text{hypothèse} \
3. & \quad p & \text{hypothèse (pour } \rightarrow I\text{)} \
4. & \quad q & \rightarrow E ; (1, 3) \
5. & \quad r & \rightarrow E ; (2, 4) \
6. & p \rightarrow r & \rightarrow I ; (3{-}5) \end{array} $$

Exemple de preuve: $\vdash p \lor \neg p$ (Tiers exclu)

En logique classique, avec la règle de double négation:

$$ \begin{array}{lll}

1. & \quad \neg(p \lor \neg p) & \text{hypothèse (pour } \neg I\text{)} \
2. & \quad \quad p & \text{hypothèse} \
3. & \quad \quad p \lor \neg p & \lor I_1 ; (2) \
4. & \quad \quad \bot & \neg E ; (1, 3) \
5. & \quad \neg p & \neg I ; (2{-}4) \
6. & \quad p \lor \neg p & \lor I_2 ; (5) \
7. & \quad \bot & \neg E ; (1, 6) \
8. & \neg\neg(p \lor \neg p) & \neg I ; (1{-}7) \
9. & p \lor \neg p & DN ; (8) \end{array} $$

Déduction naturelle pour la logique du premier ordre

Règles pour $\forall$

Introduction de $\forall$ (Généralisation):

$$ \frac{\Gamma \vdash \varphi}{\Gamma \vdash \forall x , \varphi} ; (\forall I) $$

Condition: $x$ ne doit pas apparaître libre dans $\Gamma$.

Élimination de $\forall$ (Instanciation universelle):

$$ \frac{\Gamma \vdash \forall x , \varphi}{\Gamma \vdash \varphi[t/x]} ; (\forall E) $$

où $t$ est un terme libre pour $x$ dans $\varphi$.

Règles pour $\exists$

Introduction de $\exists$ (Instanciation existentielle):

$$ \frac{\Gamma \vdash \varphi[t/x]}{\Gamma \vdash \exists x , \varphi} ; (\exists I) $$

Élimination de $\exists$:

$$ \frac{\Gamma \vdash \exists x , \varphi \quad \Gamma, \varphi[c/x] \vdash \psi}{\Gamma \vdash \psi} ; (\exists E) $$

Condition: $c$ est une constante “fraîche” n’apparaissant ni dans $\Gamma$, ni dans $\varphi$, ni dans $\psi$.

Exemple: Tout A est B, Tout B est C ⊢ Tout A est C

$$ \begin{array}{lll}

1. & \forall x (A(x) \rightarrow B(x)) & \text{hypothèse} \
2. & \forall x (B(x) \rightarrow C(x)) & \text{hypothèse} \
3. & \quad A(a) \rightarrow B(a) & \forall E ; (1) \
4. & \quad B(a) \rightarrow C(a) & \forall E ; (2) \
5. & \quad \quad A(a) & \text{hypothèse} \
6. & \quad \quad B(a) & \rightarrow E ; (3, 5) \
7. & \quad \quad C(a) & \rightarrow E ; (4, 6) \
8. & \quad A(a) \rightarrow C(a) & \rightarrow I ; (5{-}7) \
9. & \forall x (A(x) \rightarrow C(x)) & \forall I ; (8) \end{array} $$

Théorèmes méta-logiques

Correction (Soundness)

Théorème: Si $\Gamma \vdash \varphi$, alors $\Gamma \models \varphi$.

Tout ce qui est prouvable est vrai. Le système ne dérive pas de faussetés.

Complétude (Completeness)

Théorème (Gödel, 1930): Si $\Gamma \models \varphi$, alors $\Gamma \vdash \varphi$.

Tout ce qui est vrai est prouvable. Le système capture toutes les vérités logiques.

Importance

La conjonction de ces deux théorèmes établit:

$$ \Gamma \vdash \varphi \iff \Gamma \models \varphi $$

La syntaxe (preuves) et la sémantique (vérité) coïncident pour la logique du premier ordre.

Décidabilité

Théorème (Church-Turing): La logique du premier ordre est indécidable.

Il n’existe pas d’algorithme qui, pour toute formule $\varphi$, décide si $\vdash \varphi$ ou non.

Cependant, la logique du premier ordre est semi-décidable: si $\vdash \varphi$, un algorithme finira par trouver une preuve.

Stratégies de preuve

Preuve directe

Appliquer les règles en suivant la structure de la formule à prouver.

Pour prouver $\varphi \rightarrow \psi$: Supposer $\varphi$, dériver $\psi$.

Pour prouver $\varphi \land \psi$: Prouver $\varphi$ et prouver $\psi$.

Preuve par contraposition

Pour prouver $\varphi \rightarrow \psi$: prouver $\neg\psi \rightarrow \neg\varphi$.

Preuve par l’absurde

Pour prouver $\varphi$: supposer $\neg\varphi$, dériver $\bot$.

Preuve par cas

Pour utiliser $\varphi \lor \psi$: prouver séparément en supposant $\varphi$ puis $\psi$.

Théorèmes importants

Théorème de déduction

$$ \Gamma, \varphi \vdash \psi \iff \Gamma \vdash \varphi \rightarrow \psi $$

Monotonie

$$ \text{Si } \Gamma \vdash \varphi \text{ et } \Gamma \subseteq \Gamma’, \text{ alors } \Gamma’ \vdash \varphi $$

Transitivité (Cut)

$$ \text{Si } \Gamma \vdash \varphi \text{ et } \Gamma, \varphi \vdash \psi, \text{ alors } \Gamma \vdash \psi $$