Système à la Hilbert

On considère l'ensemble des formules du calcul propositionnel. Rappelons qu'il s'agit des formules finies que l'on peut construire inductivement à partir des variables propositionnelles au moyen des connecteurs logiques.

On se donne un ensemble d'axiomes logiques qui sont des formules valides du calcul propositionnel. Une déduction est une suite de formules telle que chaque formule ${\displaystyle A}$ apparaissant dans cette suite vérifie l'une des conditions suivantes :

• ${\displaystyle A}$ est une instance d'axiome (ou de théorème), c’est-à-dire l'un des axiomes logiques (ou l'un des théorèmes déjà démontrés) dans lequel les variables propositionnelles sont remplacées par des formules ;
• il existe deux formules précédant ${\displaystyle A\,}$ qui sont de la forme ${\displaystyle B\to A}$ et ${\displaystyle B\,}$ ; on dit alors que ${\displaystyle A\,}$ est obtenue par modus ponens entre ces deux formules.

On représente une déduction en écrivant les formules ligne par ligne et en adjoignant un commentaire à chaque ligne pour expliquer comment la formule correspondante a été obtenue.

Il existe plusieurs choix possibles de systèmes axiomatiques du calcul propositionnel. On en donne un ici relativement verbeux mais assez intuitif.

• Axiomes pour l'implication. Le choix de ces deux axiomes un peu étranges se justifie par le fait qu'ils simplifient la démonstration du théorème de déduction :
  • Axiome ${\displaystyle K}$ : ${\displaystyle f\to (g\to f)}$ ;
  • Axiome ${\displaystyle S}$ : ${\displaystyle (f\to (g\to h))\to ((f\to g)\to (f\to h))}$.

• Axiomes pour la négation. On donne deux des principales variantes de ces axiomes ; à titre d'exemple le lecteur pourra choisir l'une d'elles et essayer de trouver une déduction de l'autre :
  • Raisonnement par l'absurde : ${\displaystyle (\neg f\to g)\to ((\neg f\to \neg g)\to f)}$ ;
  • Contraposition : ${\displaystyle (\neg g\to \neg f)\to (f\to g)}$.

• Axiomes pour la conjonction :
  • ${\displaystyle f\to (g\to f\land g)}$ ;
  • ${\displaystyle f\land g\to f}$, ${\displaystyle f\land g\to g}$.

• Axiomes pour la disjonction :
  • ${\displaystyle f\to f\lor g}$, ${\displaystyle g\to f\lor g}$ ;
  • Raisonnement par cas : ${\displaystyle f\lor g\to ((f\to h)\to ((g\to h)\to h))}$.

Voici une déduction de l'identité ${\displaystyle f\to f}$ :

En prenant l'axiome ${\displaystyle S}$: ${\displaystyle (f\to (g\to h))\to ((f\to g)\to (f\to h))}$ , et en y remplaçant ${\displaystyle g}$ par ${\displaystyle (g\to f)}$ et ${\displaystyle h}$ par ${\displaystyle f}$, on obtient :

1. ${\displaystyle (f\to ((g\to f)\to f))\to ((f\to (g\to f))\to (f\to f))}$ (instance de l'axiome ${\displaystyle S}$)

   Puis en prenant l'axiome ${\displaystyle K}$: ${\displaystyle f\to (g\to f)}$ et en y remplaçant ${\displaystyle g}$ par ${\displaystyle (g\to f)}$, on obtient :

2. ${\displaystyle f\to ((g\to f)\to f)}$ (instance de l'axiome ${\displaystyle K}$)
3. ${\displaystyle (f\to (g\to f))\to (f\to f)}$ (modus ponens entre 1 et 2)
4. ${\displaystyle f\to (g\to f)}$ (instance de l'axiome ${\displaystyle K}$)
5. ${\displaystyle f\to f}$ (modus ponens entre 3 et 4)

Comme on voit sur l'exemple précédent, il est assez malcommode de démontrer les propriétés les plus simples. C'est pourquoi on étend le système en ajoutant la possibilité d'utiliser des hypothèses, c’est-à-dire des formules non prouvées. Ainsi au lieu de démontrer ${\displaystyle f\to f}$, on se contenterait de démontrer ${\displaystyle f\,}$ en utilisant l'hypothèse ${\displaystyle f\,}$, ce qui revient à écrire une démonstration d'une seule ligne.

Un autre exemple de démonstration avec hypothèse est donné par la transitivité de l'implication : en se donnant les hypothèses ${\displaystyle f\to g}$, ${\displaystyle g\to h}$ et ${\displaystyle f\,}$, on démontre que ${\displaystyle h\,}$ :

1. ${\displaystyle f\,}$ (hypothèse)
2. ${\displaystyle f\to g}$ (hypothèse)
3. ${\displaystyle g\,}$ (modus ponens entre 2 et 1)
4. ${\displaystyle g\to h}$ (hypothèse)
5. ${\displaystyle h\,}$ (modus ponens entre 4 et 3)

La question se pose alors de savoir si à partir d'une preuve avec hypothèses on peut récupérer une preuve sans ; par exemple peut-on à partir de la preuve ci-dessus déduire l'existence d'une preuve de ${\displaystyle (f\to g)\to ((g\to h)\to (f\to h))}$ ? La réponse est oui, et c'est ce qu'énonce le théorème de déduction : si on a une démonstration d'une formule ${\displaystyle A}$ utilisant une hypothèse ${\displaystyle B}$ alors on peut construire une démonstration de ${\displaystyle B\to A}$ qui n'utilise plus cette hypothèse, soit si ${\displaystyle B\vdash A}$, alors ${\displaystyle \vdash B\to A}$.

L'utilisation du théorème de déduction permet de simplifier considérablement la recherche de preuves dans les systèmes à la Hilbert. C'est un passage obligé d'une démonstration du théorème de complétude pour un tel système. Dans la déduction naturelle ou le calcul des séquents de Gerhard Gentzen le théorème de la déduction est en quelque sorte intégré comme règle primitive sous la forme d'introduction droite de l'implication.