Système à la Hilbert

En logique, les systèmes à la Hilbert servent à définir les déductions formelles en suivant un modèle proposé par David Hilbert au début du : un grand nombre daxiomes logiques exprimant les principales propriétés de la logique que l'on combine au moyen de quelques règles, notamment la règle de modus ponens, pour dériver de nouveaux théorèmes. Les systèmes à la Hilbert héritent du système défini par Gottlob Frege et constituent les premiers systèmes déductifs, avant l'apparition de la déduction naturelle ou du calcul des séquents, appelés parfois par opposition systèmes à la Gentzen. 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 apparaissant dans cette suite vérifie l'une des conditions suivantes : 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 qui sont de la forme et ; on dit alors que 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 : ; Axiome : . 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 : ; Contraposition : .