Style de Fitch pour la déduction naturelle

Les règles exposées dans ce paragraphe sont celles du calcul des propositions. Elles permettent d’enchaîner logiquement les phrases, c’est-à-dire d'introduire de nouvelles phrases comme conséquences logiques de ce qui a été dit auparavant. À chacun des opérateurs logiques fondamentaux sont associées deux règles de déduction. L'une des règles est une règle d'introduction : elle explique comment prouver une proposition possédant l'opérateur. L'autre règle est une règle d'élimination : elle explique comment utiliser une proposition possédant l'opérateur pour poursuivre le raisonnement.

Introduction et élimination sont nécessaires pour pouvoir démonter et remonter des formules. La recherche d’une déduction logique consiste justement à analyser les prémisses, c’est-à-dire à les démonter, et à réassembler les morceaux pour faire des formules que l’on peut enchainer logiquement jusqu’à la conclusion. On croit parfois qu’il est très difficile de faire des preuves mathématiques, mais dans son principe, ce n’est pas très différent d’un jeu de construction avec des cubes.

La règle d'introduction de l'implication ou règle de l'abandon d'une hypothèse provisoire énonce que, pour prouver une implication « si P alors Q », il suffit de procéder de la façon suivante : on pose P comme hypothèse provisoire, on fait alors des déductions à partir de toutes les phrases antérieures plus P en vue d’atteindre Q. Une fois Q atteint, on peut alors en déduire « si P alors Q ». Insistons sur un point : Q est démontrée sous l’hypothèse P mais « si P alors Q », elle, ne dépend que des prémisses antérieures. Si on utilise la méthode de Fitch, on peut introduire n’importe quand dans une déduction une hypothèse provisoire. Il suffit de la décaler vers la droite par rapport aux autres prémisses. Tout ce qui est déduit sous une hypothèse provisoire doit être sous elle ou sur sa droite mais jamais sur sa gauche. La règle d'introduction permet de conclure qu'on a prouvé « si P alors Q » sans l'hypothèse P. On peut décaler « si P alors Q » sur la gauche par rapport à P, mais pas par rapport aux autres prémisses utilisées dans la démonstration de Q. On notera :

${\displaystyle 1\quad \quad P}$ (hypothèse provisoire)

${\displaystyle 2\quad \quad Q}$ (propriété déduite de 1)

${\displaystyle 3\quad P\to Q}$ (introduction de l'implication entre les deux lignes 1 et 2)

La règle d'élimination de l'implication, ou règle du détachement ou du modus ponens énonce que, des deux phrases « P » et « si P alors Q » on peut déduire « Q ». Elle permet de passer de conditions déjà connues, P, à des conditions nouvelles, Q, pourvu qu’il y ait une loi qui l’autorise, « si P alors Q », ce qui sera noté :

${\displaystyle 1\quad P}$

${\displaystyle 2\quad P\to Q}$

${\displaystyle 3\quad Q}$ (élimination de l'implication entre les lignes 1 et 2)

Montrons par exemple qu’avec ces deux règles on peut déduire « si P alors R » à partir des deux phrases « si P alors Q » et « si Q alors R » :

${\displaystyle 1\quad P\to Q}$ (hypothèse)

${\displaystyle 2\quad Q\to R}$ (hypothèse)

${\displaystyle 3\quad \quad P}$ (hypothèse provisoire)

${\displaystyle 4\quad \quad Q}$ (modus ponens sur 3 et 1)

${\displaystyle 5\quad \quad R}$ (modus ponens sur 4 et 2)

${\displaystyle 6\quad P\to R}$(règle d'introduction de l'implication entre 3 et 5, abandon de l’hypothèse provisoire P).

Pour la conjonction, les règles sont très simples.

La règle d'introduction de la conjonction énonce que, à partir des deux phrases A et B on peut déduire la phrase (A et B).

${\displaystyle 1\quad A}$

${\displaystyle 2\quad B}$

${\displaystyle 3\quad A\land B}$ (introduction de la conjonction entre 1 et 2)

La règle d'élimination de la conjonction énonce que, à partir de la phrase (A et B), on peut déduire les deux phrases A et B prises séparément.

${\displaystyle 1\quad A\land B}$

${\displaystyle 2\quad A}$ (élimination de la conjonction 1)

${\displaystyle 3\quad B}$ (élimination de la conjonction 1)

Ces règles permettent d'assembler ou au contraire de séparer des assertions qui sont toutes considérées comme vraies. C’est la forme logique de la capacité de la raison à analyser le monde, c’est-à-dire à étudier ses parties séparément, et à le synthétiser, c’est-à-dire à rassembler les éléments d’une étude en un tout. C’est pourquoi ces règles sont également appelées les règles de l'analyse et de la synthèse.

Les deux règles de déduction pour la disjonction sont les suivantes.

La règle d'introduction de la disjonction ou règle de l'affaiblissement d'une thèse énonce que, à partir de la phrase P on peut déduire la phrase (P ou Q) aussi bien que la phrase (Q ou P), quelle que soit la phrase Q. Cette règle peut sembler peu intéressante mais elle est en vérité très importante. Parfois il est avantageux de déduire (P ou Q) après avoir prouvé P, car on peut savoir par ailleurs que (P ou Q) a d'autres conséquences.

${\displaystyle 1\quad P}$

${\displaystyle 2\quad P\lor Q}$ (introduction de la disjonction à partir de 1)

et de même

${\displaystyle 1\quad Q}$

${\displaystyle 2\quad P\lor Q}$ (introduction de la disjonction à partir de 1)

La règle d'élimination de la disjonction ou règle de la disjonction des hypothèses ou règle de la distinction des cas, stipule que, si on a prouvé (P ou Q) et qu'on a également prouvé (si P alors R) ainsi que (si Q alors R), alors on a prouvé R. Cette règle sert quand on examine plusieurs cas possibles qui conduisent à la même conclusion.

${\displaystyle 1\quad P\lor Q}$

${\displaystyle 2\quad \quad P}$ (hypothèse provisoire)

${\displaystyle 3\quad \quad R}$ (propriété déduite de 2)

${\displaystyle 4\quad P\to R}$ (introduction de l'implication entre 2 et 3)

${\displaystyle 5\quad \quad Q}$ (hypothèse provisoire)

${\displaystyle 6\quad \quad R}$ (propriété déduite de 5)

${\displaystyle 7\quad Q\to R}$ (introduction de l'implication entre 5 et 6)

${\displaystyle 8\quad R}$ (élimination de la disjonction entre 1, 4, 7)

La règle d'introduction de la négation énonce que, si on démontre une contradiction à partir d’une hypothèse P alors celle-ci est nécessairement fausse et donc sa négation est vraie. Ainsi, si dans une déduction sous l’hypothèse provisoire P, on a trouvé une contradiction (Q et non Q), notée également ${\displaystyle \bot }$, alors on peut déduire nonP à partir de toutes les prémisses antérieures sauf P. Avec la méthode de Fitch, on décale donc (non P) sur la gauche par rapport à P, ce qui se représente comme suit :

${\displaystyle 1\quad \quad \quad P}$

${\displaystyle 2\quad \quad \quad \bot }$

${\displaystyle 3\quad \lnot P}$ (introduction de la négation entre 1 et 2)

La règle d'élimination de la négation ou règle de la suppression de la double-négation ou raisonnement par absurde énonce que, de (non nonP) on peut déduire P. Il s'agit bien du raisonnement par l'absurde car dans, un tel raisonnement, pour prouver P, on suppose (non P) et l'on cherche à obtenir une contradiction. Si tel est le cas, on a prouvé (non non P) d'après la règle d'introduction de la négation, et c'est bien la règle de suppression de la double-négation qui permet de conclure à P :

${\displaystyle 1\quad \lnot \lnot P}$

${\displaystyle 2\quad P}$ (élimination de la double négation 1)

ou bien

${\displaystyle 1\quad \quad \lnot P}$ (hypothèse provisoire [raisonnement par l'absurde])

${\displaystyle 2\quad \quad \bot }$

${\displaystyle 3\quad \lnot \lnot P}$ (introduction de la négation entre 1 et 2)

${\displaystyle 4\quad P}$ (élimination de la double négation 3)

Quand on considère que toute phrase est nécessairement ou bien vraie ou bien fausse, la validité de cette dernière règle est évidente. Elle est caractéristique de la logique classique, qui est présentée ici et est utilisée par la grande majorité des scientifiques. Elle est parfois contestée à cause d’un problème important, celui des preuves d’existence par l’absurde. Il arrive que l’on puisse prouver qu’un problème a une solution sans être capable de la trouver. Pour cela il suffit de prouver que l’absence de solution conduit à une contradiction. Le raisonnement par l’absurde permet alors de conclure qu’il n’est pas vrai que le problème n’a pas de solution : non non (le problème a une solution). En logique classique, on supprime la double négation pour en conclure que le problème a une solution. Cependant, la démarche ainsi suivie ne fournit aucun procédé constructif de la solution cherchée. Cette objection fut soulevée par certains mathématiciens et logiciens, dont Brouwer, qui contestèrent cette méthode et s'opposèrent à Hilbert qui la défendait. Les mathématiciens constructivistes ou intuitionnistes estiment qu’une preuve d’existence n’a pas de sens si elle ne fournit pas également un procédé constructif de l'objet en question. Aussi ces derniers rejettent-ils la règle de suppression de la double négation pour lui substituer la règle suivante : de P et (non P), on peut déduire une contradiction, et de cette contradiction n'importe quelle proposition Q (principe du ex falso quodlibet).

${\displaystyle 1\quad P}$

${\displaystyle 2\quad \lnot P}$

${\displaystyle 3\quad \bot }$

${\displaystyle 4\quad Q}$ (élimination de la négation 2 en logique intuitionniste)

Dans les exemples, nous utiliserons cette deuxième règle d'élimination lorsqu'il est possible de se passer de la règle d'élimination de la double négation

On peut introduire d’autres règles pour les autres opérateurs booléens, notamment l’opérateur d’équivalence, mais ce n’est pas nécessaire, parce que ces opérateurs peuvent être définis à partir des précédents et que leurs règles de déduction peuvent être alors déduites à partir des règles précédentes. (P équivaut à Q) est défini par ( (si P alors Q) et (si Q alors P) ) .

Nous donnons ci-dessous quelques exemples d'utilisation de la déduction naturelle. Dans la première partie, nous n'utiliserons pas la règle d'élimination de la double négation. Dans la deuxième partie, nous utiliserons cette règle. Les formules déduites dans cette deuxième partie ne sont pas reconnues valides par les mathématiciens intuitionnistes. Nous utiliserons les symboles suivants : ${\displaystyle \to }$ pour si ... alors ..., ${\displaystyle \lor }$ pour ou, ${\displaystyle \land }$ pour et, ${\displaystyle \lnot }$ pour non. Le symbole ${\displaystyle \bot }$ désigne une contradiction, c'est-à-dire une proposition fausse.

Exemple 1 : ${\displaystyle (\lnot A\land \lnot B)\to \lnot (A\lor B)}$

${\displaystyle 01\quad \quad \lnot A\land \lnot B}$ (hypothèse provisoire)

${\displaystyle 02\quad \quad \lnot A}$ (élimination de la conjonction 01)

${\displaystyle 03\quad \quad \lnot B}$ (élimination de la conjonction 01)

${\displaystyle 04\quad \quad \quad A\lor B}$ (hypothèse provisoire)

${\displaystyle 05\quad \quad \quad \quad A}$ (hypothèse provisoire)

${\displaystyle 06\quad \quad \quad \quad \bot }$contradiction entre 02 et 05

${\displaystyle 07\quad \quad \quad A\to \bot }$ (introduction de l'implication entre 05 et 06)

${\displaystyle 08\quad \quad \quad \quad B}$ (hypothèse provisoire)

${\displaystyle 09\quad \quad \quad \quad \bot }$ contradiction entre 03 et 08

${\displaystyle 10\quad \quad \quad B\to \bot }$ (introduction de l'implication entre 08 et 09)

${\displaystyle 11\quad \quad \quad \bot }$ (élimination de la disjonction entre 04, 07, 10)

${\displaystyle 12\quad \quad \lnot (A\lor B)}$ (introduction de la négation entre 04 et 11)

${\displaystyle 13\quad (\lnot A\land \lnot B)\to \lnot (A\lor B)}$ (introduction de l'implication entre 01 et 12 et fin de la déduction)

On montre que la réciproque ${\displaystyle \lnot (A\lor B)\to (\lnot A\land \lnot B)}$ est également valide. On montre également que ${\displaystyle (\lnot A\lor \lnot B)\to \lnot (A\land B)}$, mais pour la réciproque de cette dernière propriété, on utilise l'élimination de la double négation.

Exemple 2 : ${\displaystyle A\to \lnot \lnot A}$

${\displaystyle 01\quad \quad A}$ (hypothèse provisoire)

${\displaystyle 02\quad \quad \quad \lnot A}$ (hypothèse provisoire)

${\displaystyle 03\quad \quad \quad \bot }$ (élimination de la négation entre 01 et 02)

${\displaystyle 04\quad \quad \lnot \lnot A}$ (introduction de la négation entre 02 et 03)

${\displaystyle 05\quad A\to \lnot \lnot A}$ (introduction de l'implication entre 01 et 04, fin de la déduction)

La réciproque ${\displaystyle \lnot \lnot A\to A}$ découle directement de l'élimination de la double négation et est rejetée par les intuitionnistes. Mais curieusement, il n'en est pas de même de ${\displaystyle \lnot \lnot \lnot A\to \lnot A}$ qui se prouve sans cette hypothèse, et qui, elle, est acceptée par les intuitionnistes.

Exemple 3 : ${\displaystyle \lnot \lnot \lnot A\to \lnot A}$

${\displaystyle 01\quad \quad \lnot \lnot \lnot A}$ (hypothèse provisoire)

${\displaystyle 02\quad \quad \quad A}$ (hypothèse provisoire)

${\displaystyle 03\quad \quad \quad A\to \lnot \lnot A}$ (théorème de l'exemple 2)

${\displaystyle 04\quad \quad \quad \lnot \lnot A}$ (élimination de l'implication ou modus ponens entre 02 et 03)

${\displaystyle 05\quad \quad \quad \bot }$ (élimination de la négation entre 01 et 04)

${\displaystyle 06\quad \quad \lnot A}$ (introduction de la négation entre 02 et 05)

${\displaystyle 07\quad \lnot \lnot \lnot A\to \lnot A}$ (introduction de l'implication entre 01 et 06, fin de la déduction)

Les exemples qui suivent utilisent l'élimination de la double négation. On peut montrer que cette utilisation est nécessaire. Ils ne sont donc pas acceptés en logique intuitionniste.

Exemple 4 : ${\displaystyle \lnot (A\land B)\to (\lnot A\lor \lnot B)}$

${\displaystyle 01\quad \quad \lnot (A\land B)}$ (hypothèse provisoire [raisonnement par l'absurde])

${\displaystyle 02\quad \quad \quad \lnot (\lnot A\lor \lnot B)}$ (hypothèse provisoire)

${\displaystyle 03\quad \quad \quad \lnot (\lnot A\lor \lnot B)\to (\lnot \lnot A\land \lnot \lnot B)}$ (théorème, réciproque de l'exemple 1)

${\displaystyle 04\quad \quad \quad \lnot \lnot A\land \lnot \lnot B}$ (élimination de l'implication ou modus ponens entre 02 et 03)

${\displaystyle 05\quad \quad \quad A\land B}$ (élimination de la double négation dans 04)

${\displaystyle 06\quad \quad \quad \bot }$ (élimination de la négation entre 01 et 05)

${\displaystyle 07\quad \quad \lnot \lnot (\lnot A\lor \lnot B)}$ (introduction de la négation entre 02 et 06)

${\displaystyle 08\quad \quad \lnot A\lor \lnot B}$ (élimination de la double négation dans 07)

${\displaystyle 09\quad \lnot (A\land B)\to (\lnot A\lor \lnot B)}$ (introduction de l'implication entre 01 et 08)

Exemple 5 : si ${\displaystyle (A\to B)\to (\lnot B\to \lnot A)}$ ne nécessite pas l'élimination de la double négation, celle-ci est nécessaire pour prouver la réciproque ${\displaystyle (\lnot B\to \lnot A)\to (A\to B)}$.

Exemple 6: On peut démontrer que ${\displaystyle \lnot A\to (A\to B)}$. En effet si on ${\displaystyle \lnot A}$ et ${\displaystyle A}$, on a ${\displaystyle \bot }$ (faux) et donc on a ${\displaystyle B}$.

Exemple 7 : de même la démonstration de la validité du tiers exclu ${\displaystyle A\lor \lnot A}$ utilise l'élimination de la double négation. En supposant que ${\displaystyle \lnot (A\lor \lnot A)}$, on en déduit ${\displaystyle \lnot A\land \lnot \lnot A}$ (réciproque de l'exemple 1), d'où une contradiction et la validité de ${\displaystyle \lnot \lnot (A\lor \lnot A)}$.

Si les intuitionnistes rejettent le tiers exclu, ils acceptent bien sûr le principe de non contradiction : ${\displaystyle \lnot (A\land \lnot A)}$. En effet, la supposition ${\displaystyle A\land \lnot A}$ est une contradiction. On a donc ${\displaystyle \lnot (A\land \lnot A)}$ par introduction de la négation.

Exemple 7 connu sous le nom de loi de Peirce : ${\displaystyle ((A\to B)\to A)\to A}$. Curieusement, bien que ne contenant pas de négation, la déduction de cette loi nécessite l'élimination de la double négation, par exemple par l'intermédiaire de l'utilisation du tiers exclu. On suppose que l'on a ${\displaystyle ((A\to B)\to A)}$. D'après le tiers exclu:

• ou bien on a ${\displaystyle A}$,
• ou bien on a ${\displaystyle \lnot A}$ et donc on a ${\displaystyle A\to B}$ (exemple 6) et puisqu'on a ${\displaystyle ((A\to B)\to A)}$ avec le modus ponens, on a ${\displaystyle A}$.