Théorème de la déduction : démonstration (preuve)

Théorème de la Déduction
Contexte : Systèmes de Déduction

En logique propositionnelle et en logique du premier ordre, un système de déduction est un ensemble de règles permettant de dériver des formules (théorèmes) à partir d’un ensemble d’axiomes.

La notation $T \cup \{A\} \vdash B$ signifie qu’il existe une démonstration formelle de la formule $B$ en utilisant les axiomes de la théorie $T$, la formule $A$ comme hypothèse supplémentaire, et les règles d’inférence du système (typiquement, le modus ponens).

Théorème de la Déduction (Herbrand-Tarski)

Soient $T$ une théorie (un ensemble de formules) et $A$ et $B$ deux formules. Si la formule $B$ est démontrable à partir de la théorie $T$ augmentée de l’hypothèse $A$, alors l’implication $A \to B$ est démontrable à partir de la théorie $T$ seule. $$ T \cup \{A\} \vdash B \implies T \vdash (A \to B) $$

Remarque

La réciproque, $T \vdash (A \to B) \implies T \cup \{A\} \vdash B$, est une conséquence directe de la règle d’inférence du modus ponens et est généralement beaucoup plus simple à établir. Le cœur du théorème est bien l’implication énoncée ci-dessus.

Démonstration (pour la logique propositionnelle)

La démonstration se fait par induction sur la longueur de la preuve de $B$ à partir de $T \cup \{A\}$. Soit $B_1, B_2, \dots, B_n = B$ une telle preuve. Nous allons montrer par récurrence que pour chaque étape $k$ de la preuve (de 1 à $n$), on a $T \vdash (A \to B_k)$.

Cas de base (k=1)

La première formule $B_1$ de la preuve doit être soit un axiome logique, soit un axiome de la théorie $T$, soit l’hypothèse $A$ elle-même.

  • Si $B_1$ est un axiome (logique ou de T) : On sait que $T \vdash B_1$. Or, dans la plupart des systèmes logiques, on a le schéma d’axiome $X \to (Y \to X)$. En posant $X=B_1$ et $Y=A$, on a $T \vdash (B_1 \to (A \to B_1))$. Par modus ponens avec $T \vdash B_1$, on conclut que $T \vdash (A \to B_1)$.
  • Si $B_1$ est l’hypothèse $A$ : On veut montrer que $T \vdash (A \to A)$. C’est un théorème de base dans tous les systèmes de logique propositionnelle.

Étape d’induction

Supposons que pour tout $i < k$, on ait déjà démontré que $T \vdash (A \to B_i)$. Montrons que $T \vdash (A \to B_k)$.

La formule $B_k$ peut apparaître dans la preuve pour trois raisons :

  1. $B_k$ est un axiome ou un élément de $T$ : Le raisonnement est le même que pour le cas de base.
  2. $B_k$ est l’hypothèse $A$ : Le raisonnement est le même que pour le cas de base.
  3. $B_k$ est obtenue par modus ponens : C’est le cas le plus important. Il existe deux formules antérieures dans la preuve, disons $B_i$ et $B_j$ (avec $i, j < k$), telles que $B_j$ est de la forme $B_i \to B_k$.

    Par hypothèse de récurrence, nous savons que :

    • $T \vdash (A \to B_i)$
    • $T \vdash (A \to (B_i \to B_k))$

    Or, un des axiomes standards de la logique propositionnelle est l’axiome de distribution : $(X \to (Y \to Z)) \to ((X \to Y) \to (X \to Z))$.

    En posant $X=A$, $Y=B_i$, et $Z=B_k$, cet axiome nous donne :

    $$ T \vdash (A \to (B_i \to B_k)) \to ((A \to B_i) \to (A \to B_k)) $$ En appliquant le modus ponens une première fois avec notre hypothèse de récurrence $T \vdash (A \to (B_i \to B_k))$, on obtient : $$ T \vdash ((A \to B_i) \to (A \to B_k)) $$ En appliquant le modus ponens une seconde fois avec notre autre hypothèse de récurrence $T \vdash (A \to B_i)$, on arrive à la conclusion désirée : $$ T \vdash (A \to B_k) $$

Par induction, la propriété est donc vraie pour toutes les étapes de la preuve, et en particulier pour la dernière étape, $B_n=B$. On a donc bien montré que $T \vdash (A \to B)$.

Implications

Ce théorème est d’une importance capitale car il justifie la méthode de raisonnement la plus courante en mathématiques : pour prouver une implication « Si A, alors B », on suppose A et on en déduit B. Le théorème de la déduction garantit que cette démarche intuitive peut être formalisée en une preuve rigoureuse.