Style de Fitch pour la déduction naturelle - Définition

Comment vérifier la correction d’un raisonnement ?

A ces douze règles, ou quatorze, si on compte que la règle d'éliminination de la conjonction est en fait une double règle, et de même pour la règle d'introduction de la disjonction, il faut en ajouter une quinzième, très simple, la règle de répétition : on peut toujours répéter une thèse antérieure, sauf si elle dépend d’une hypothèse qui a été abandonnée. On peut donc répéter toutes les thèses tant qu’on ne les décale pas sur la gauche. Cette règle est nécessaire quand on veut répéter une prémisse dans une conclusion ou quand on a besoin d’une thèse antérieure dans le corps d’une déduction sous hypothèse provisoire pour appliquer une règle.

La liste des quinze règles précédentes est complète au sens où elle suffit pour faire toutes les déductions correctes. Kurt Gödel a prouvé, (Théorème de complétude) pour un système logique différent, mais équivalent à celui qui vient d’être présenté, qu’il suffit pour formaliser toutes les déductions correctes du Calcul des prédicats du premier ordre.

Les déductions correctes sont d’abord toutes celles qui respectent rigoureusement ces règles fondamentales. Toutes les phrases doivent être ou bien des axiomes, ou bien des hypothèses provisoires, ou bien des conséquences des phrases qui les précèdent en vertu de l’une des quinze règles. Par souci de rapidité, on peut également utiliser des règles dérivées (par exemple faire suivre par ). Une règle dérivée est correcte lorsqu’on peut montrer que tout ce qui peut être déduit avec elle peut aussi être déduit sans elle avec seulement les règles fondamentales.

Tant que les déductions sont formalisées, il est toujours possible de reconnaitre, y compris par un programme, si une déduction est correcte parce que les règles de déduction sont en nombre fini et qu’il est toujours possible de vérifier en un temps fini si une formule est la conséquence d’une ou plusieurs autres en vertu de l’une de ces règles. Cette démarche réalise une partie du programme appelé parfois finitaire proposé par David Hilbert pour résoudre les problèmes des fondements des mathématiques. Hilbert cherchait une méthode efficace qui permette de décider pour tout énoncé mathématique s'il est un théorème, c’est-à-dire une vérité mathématique. Le calcul des prédicats permettait de ramener le problème à la question de savoir si une formule est une loi logique ou non.

Mais s'il est possible de vérifier la validité d'une déduction conduisant à une formule, à l'inverse, la question de savoir si une formule donnée est une loi logique ou non ne peut être résolue en général. En effet, il n’existe pas de méthode universelle permettant de dire si une formule est une loi logique ou non. Cet inexistence se déduit du théorème d'incomplétude de Gödel. On dit que la question de savoir si une formule est une loi logique est indécidable.

La vérification de la correction des déductions dans la langue courante pose davantage de difficultés. Il faut d’abord traduire les phrases familières dans une langue formalisée du calcul des prédicats. Cette étape pose parfois problème si on a des doutes sur la fidélité de la traduction. Mais la plus grosse difficulté vient de ce que les déductions courantes font en général une large place à l’implicite. Même les relations de dépendance par rapport à une hypothèse ne sont pas toujours explicitées. Les déductions formelles au contraire ne laissent rien dans l’ombre. Celles qui sont ici proposées sont très semblables aux déductions courantes sauf qu’elles explicitent tout. Afin de certifier correct les raisonnements et démonstrations usuels il faut expliciter de tout ce qui est implicite. C’est pourquoi souvent il faut beaucoup étudier et connaître tout l’implicite avant de savoir si un raisonnement est correct.