Section 1.8

La déduction naturelle

Un tampon encreur de validation.

Jusqu'à présent, nous avons vu un unique moyen de démontrer la validité d'une proposition : vérifier que la formule vaut 1 pour toutes les interprétations possibles. Autrement dit, pour montrer qu'une proposition est toujours vraie, il nous fallait établir une table de vérité et vérifier que la colonne correspondant à la proposition ne contient bien que des 1. Cette méthode est parfois très longue, voire tout simplement inapplicable dans des logiques plus complexes tels que la logique des prédicats souvent employée en mathématiques, où il est impossible de tester toutes les interprétations possibles.

Dans cette section, nous allons étudier un système de déduction inventé par le logicien allemand Gerhard Gentzen au début du vingtième siècle et appelé la déduction naturelle. Ce système est basé sur l'idée que la validité d'une proposition peut être démontrée en appliquant des règles d'inférence. Ces règles d'inférence sont des règles de raisonnement qui permettent de déduire la validité d'une proposition à partir de celle d'autres propositions. Ce système de déduction naturelle est une manière formelle de démontrer la validité d'une proposition sans avoir à énumérer toutes ses interprétations. Nous allons voir dans cette section comment construire des preuves de propositions à l'aide de ce système.

! Remarque

Cette section est optionnelle. Le matériel présenté ici n'est pas nécessaire pour comprendre les autres sections du cours. Cependant, les lecteurs intéressés pourront trouver dans cette section des clés intéressantes pour comprendre ce qu'est une preuve mathématique, ainsi que des outils de raisonnement formel.

Il y a aussi des liens très forts entre la déduction naturelle et la programmation. Pour les plus intéressés (et téméraires), je vous conseille la lecture de la page Wikipédia sur la correspondance de Curry-Howard.

Preuve

Une preuve est un raisonnement qui permet d'établir qu'une proposition est valide. Une preuve est généralement constituée d'une suite d'étapes. À chaque étape, on montre qu'une proposition est valide à partir de la validité d'autres propositions déjà démontrées.

Parfois, une preuve utilisera des hypothèses, c'est-à-dire des propositions qu'on suppose vraies sans avoir à les démontrer. Les preuves peuvent aussi faire appel à des sous-preuves, c'est-à-dire des preuves dans la preuve, qui permettent de démontrer une proposition à partir d'une hypothèse provisoire.

Commençons par un exemple de preuve, retranscrite tout d'abord en français. La preuve cherche à démontrer que si on admet A ou B et non A, alors on peut en déduire B. La preuve est ci-dessous :

Posons comme première hypothèse A ou B et comme deuxième hypothèse non A. De la première hypothèse, on sait que A ou B est vrai. Analysons les deux cas possibles.

  • Admettons d'abord que A est vrai. Or, dans ce cas, on peut conclure à une contradiction, car A est vrai par hypothèse provisoire et non A est vrai par hypothèse. Ce cas est donc impossible, on peut donc conclure ce que l'on veut, par exemple que B est vrai.
  • Admettons maintenant que B est vrai. Alors, on peut conclure immédiatement que B est vrai par notre hypothèse provisoire.

Dans les deux cas, on peut conclure que B est vrai, ce qui conclut la preuve que B est vrai.

Ci-dessous est présenté la même preuve dans une notation appelée style de Fitch. Il s'agit d'une preuve formelle de la validité de la proposition B étant données les deux hypothèses A ou B et non A. Dans cette présentation figurent toutes les étapes qui permettent d'arriver à la conclusion. Contrairement à la preuve en français ci-dessus, chaque étape est justifiée de manière explicite par l'utilisation d'une règle d'inférence nommée. Chaque étape est très simple et ainsi peut être facilement vérifiée par un lecteur ou même un ordinateur.

L'exemple ci-dessus montre comment on peut démontrer la validité de la proposition B (ligne 8) étant données les deux hypothèses A ou B et non A (lignes 1 et 2). La preuve est constituée de plusieurs étapes. À chaque étape, on utilise une règle d'inférence pour montrer qu'une proposition est valide à partir de la validité d'autres propositions déjà démontrées.

Les lignes 3-5, ainsi que les lignes 6-7, sont ce qu'on appelle des sous-preuves. Les sous-preuves permettent d'assumer temporairement une hypothèse (appelée hypothèse provisoire) afin d'arriver à une certaine conclusion. Pour la sous-preuve des lignes 3-5, l'hypothèse provisoire est A (ligne 3) et la conclusion est B (ligne 5). Pour la sous-preuve des lignes 6-7, l'hypothèse provisoire est B (ligne 6) et la conclusion est B (ligne 7). Ces sous-preuves peuvent être référencées dans la suite de la preuve, mais les propositions qu'elles contiennent ne sont pas considérées comme démontrées en dehors de ces sous-preuves. En effet, elles ne sont valides que si l'hypothèse provisoire est vraie.

Pour clarifier la présentation sur cette page, on utilise un code couleur pour distinguer les hypothèses des étapes qui découlent d'un raisonnement logique. Les hypothèses sont des propositions qu'on suppose vraies sans avoir à les démontrer.

! Remarque

Les preuves notées sur cette pages sont notées dans un style appelé style Fitch. Ce style a été inventé par le logicien américain Frederic Brenton Fitch.

★ À essayer

Vous pouvez reproduire les preuves vues sur cette page, et en créer de nouvelles, en utilisant l'assistant de preuve disponible sur ce site.

Règle d'inférence

Une règle d'inférence est une règle de raisonnement qui permet d'établir qu'une proposition est valide à partir de la validité d'autres propositions. Les différentes règles d'inférence sont présentées ci-dessous, chacune accompagnée d'un exemple.

Hypothèse

La règle d'inférence Hypothèse permet d'ajouter une hypothèse à une preuve. Une hypothèse est une proposition qu'on suppose vraie sans avoir à la démontrer. On peut ensuite utiliser cette hypothèse pour démontrer d'autres propositions.

Les hypothèses sont mises en jaune pour les distinguer des autres propositions. Il est en effet important de pouvoir les distinguer des autres propositions car elles ne sont pas démontrées mais simplement admises.

Répétition

La règle d'inférence Répétition permet de répéter une proposition déjà démontrée. Cette règle est utile pour réutiliser une proposition déjà démontrée plus tôt dans la preuve.

Dans l'exemple ci-dessus, la ligne 2 est prouvée en utilisant la règle d'inférence Répétition. La ligne 2 est une répétition de la ligne 1. Le numéro de la ligne reproduite est indiqué après le nom de la règle d'inférence.

Introduction de vrai

La règle d'inférence Introduction de vrai permet de démontrer la proposition vrai sans avoir à utiliser d'autres propositions.

Dans l'exemple ci-dessus, la ligne 1 est directement validée par la règle d'inférence Introduction de vrai.

On appelle cette règle une règle d'introduction car elle permet d'introduire la proposition vrai dans une preuve.

Élimination de faux

La règle d'inférence Élimination de faux permet de démontrer n'importe quelle proposition à partir de la proposition faux.

Dans l'exemple ci-dessus, la ligne 2 est démontrée à partir de la ligne 1 en utilisant la règle d'inférence Élimination de faux.

La règle d'inférence Élimination de faux est une règle très puissante. Elle permet de démontrer n'importe quelle proposition à partir d'une contradiction. On appelle aussi cette règle le principe d'explosion.

Introduction de non

La règle d'inférence Introduction de non permet de démontrer une proposition de la forme non p, pour n'importe quelle proposition p, à partir d'une sous-preuve qui aboutit à une contradiction en admettant de l'hypothèse provisoire p.

Plus simplement, la règle stipule que si l'on peut démontrer une contradiction en supposant p, alors on peut démontrer non p.

Dans l'exemple ci-dessus, la ligne 3 est démontrée à partir de la sous-preuve des lignes 1 à 2. Cette sous-preuve prend l'hypothèse P et aboutit à une contradiction.

Élimination de non

La règle d'inférence Élimination de non permet de démontrer une contradiction (c'est-à-dire la proposition faux) à partir d'une proposition de la forme non p et de la proposition p.

Dans l'exemple ci-dessus, la ligne 3, qui contient la proposition faux, est démontrée à partir des lignes 1 et 2 qui contiennent une proposition et sa négation.

Introduction de et

La règle d'inférence Introduction de et permet de démontrer une proposition de la forme p et q, à partir des propositions p et q déjà démontrées.

Plus simplement, la règle stipule que si l'on peut démontrer deux propositions p et q, alors on peut démontrer p et q.

Dans l'exemple ci-dessus, la ligne 3 est démontrée à partir des lignes 1 et 2 en utilisant la règle d'inférence Introduction de et.

Élimination de et

Quand une preuve contient une proposition de la forme p et q, il est possible de démontrer p, respectivement q, en utilisant une règle d'inférence appelée Élimination de et. Cette règle existe en deux variantes : Élimination gauche de et et Élimination droite de et, selon que l'on souhaite garder la partie gauche ou droite de la conjonction.

Dans l'exemple ci-dessus, la ligne 2 est démontrée à partir de la ligne 1 en utilisant la règle d'inférence Élimination gauche de et. De même, la ligne 3 est démontrée à partir de la ligne 1 en utilisant la règle d'inférence Élimination droite de et.

Introduction de ou

La règle d'inférence Introduction de ou permet de démontrer une proposition de la forme p ou q, à partir d'une proposition p ou d'une proposition q déjà démontrée.

De manière intuitive, la règle stipule que l'on peut démontrer un disjonction p ou q en démontrant p ou en démontrant q.

Cette règle existe elle aussi en deux variantes : Introduction gauche de ou et Introduction droite de ou, selon que l'on souhaite introduire la disjonction à partir de la partie gauche ou droite.

Dans la preuve ci-dessus, la ligne 2 est démontrée à partir de la ligne 1 en utilisant la règle d'inférence Introduction gauche de ou. De même, la ligne 3 est démontrée à partir de la ligne 1 en utilisant la règle d'inférence Introduction droite de ou.

Élimination de ou

La règle d'inférence Élimination de ou permet de faire ce qu'on appelle un raisonnement par cas. Étant donnée une proposition de la forme p ou q, on peut démontrer une autre proposition r en démontrant que l'on peut démontrer r à partir de p et que l'on peut aussi démontrer r à partir de q.

Autrement, si on sait qu'une de deux propositions p ou q est vraie, et que dans les deux cas on peut démontrer r, alors on peut démontrer r.

Dans l'exemple ci-dessus, la ligne 6 est démontrée à l'aide de la règle d'inférence Élimination de ou à partir de la ligne 1 et des sous-preuves des lignes 2-3 et 4-5. La ligne 1 établit que A ou B est vraie. La sous-preuve des lignes 2-3 établit que B ou A est vraie si A est vraie. De même, la sous-preuve des lignes 4-5 établit que B ou A est vraie si B est vraie. Ainsi, on peut déduire que B ou A est vraie dans tous les cas.

Introduction de implique

La règle d'inférence Introduction de implique permet de démontrer une proposition de la forme p implique q, à partir d'une sous-preuve qui aboutit à la proposition q en admettant de l'hypothèse provisoire p.

Dans l'exemple ci-dessus, la ligne 3 est démontrée en utilisant la règle d'inférence Introduction de implique à partir de la sous-preuve des lignes 1 à 2. Dans cette sous-preuve, on a établit qu'il était possible de démontrer B en admettant de l'hypothèse provisoire A. Ainsi, on peut déduire que A implique B est vraie.

Élimination de implique

La règle d'inférence Élimination de implique permet de démontrer une proposition de la forme q, à partir d'une proposition de la forme p implique q et d'une proposition de la forme p.

Autrement dit, si on sait que p implique q est vraie, et que p est vraie, alors on peut déduire que q est vraie.

Cette règle de raisonnement est aussi connue sous son nom latin : modus ponens.

Dans l'exemple ci-dessus, la ligne 3 est démontrée en utilisant la règle d'inférence Élimination de implique à partir des lignes 1 et 2. La ligne 1 stipule que A implique B est vraie, et la ligne 2 stipule que A est vraie. Ensemble, ces deux lignes permettent de déduire que B est vraie.

Introduction de ssi

La règle d'inférence Introduction de ssi permet de démontrer une proposition de la forme p ssi q, à partir de deux implications : p implique q et q implique p.

En effet, deux propositions p et q sont équivalentes si p implique q et q implique p sont toutes les deux vraies.

Dans l'exemple ci-dessus, la ligne 3 est démontrée en utilisant la règle d'inférence Introduction de ssi à partir des lignes 1 et 2.

Élimination de ssi

La règle d'inférence Élimination de ssi permet d'obtenir deux implications à partir d'une proposition de la forme p ssi q. La règle a deux variantes : Élimination gauche de ssi, qui permet d'obtenir p implique q, et Élimination droite de ssi, qui permet d'obtenir q implique p.

Dans l'exemple ci-dessus, la ligne 2 est démontrée par la règle d'inférence Élimination gauche de ssi, alors que la ligne 3 est démontrée par la règle d'inférence Élimination droite de ssi.

Principe du tiers exclu

Le principe du tiers exclu stipule que pour toute proposition p, la proposition p ou non p est vraie. Autrement dit, une proposition est soit vraie, soit fausse. Il n'y a pas de troisième possibilité.

Dans l'exemple ci-dessus, la ligne 1 est démontrée en utilisant la règle d'inférence Principe du tiers exclu.

Raisonnement par l'absurde

La règle d'inférence Raisonnement par l'absurde permet de démontrer une proposition de la forme p, à partir d'une sous-preuve qui aboutit à une contradiction en admettant de l'hypothèse provisoire non p.

La règle est similaire à la règle d'inférence Introduction de non, mais elle permet de démontrer une proposition p au lieu de non p.

On appelle aussi cette règle réduction à l'absurde. On admet qu'une proposition est vraie parce que sa négation est fausse.

Dans l'exemple ci-dessus, la ligne 3 est démontrée en utilisant la règle d'inférence Raisonnement par l'absurde à partir de la sous-preuve des lignes 1-2. Cette sous-preuve prend l'hypothèse non A et aboutit à une contradiction.

Élimination de la double négation

Finalement, la règle d'inférence Élimination de la double négation permet de démontrer une proposition de la forme p, à partir d'une proposition de la forme non (non p). La règle stipule que quelque chose d'irréfutable est vrai.

Dans l'exemple ci-dessus, la ligne 2 est démontrée en utilisant la règle d'inférence Élimination de la double négation à partir de la ligne 1.

Exemple de preuve

Pour illustrer l'utilisation des règles d'inférence en déduction naturelle, nous allons démontrer une des lois de De Morgan, à savoir l'équivalence entre non (A et B) et (non A) ou (non B).

Complétude et correction

Prises ensemble, les règles qui forment la déduction naturelles permettent de démontrer certaines propositions. De manière intéressante, ce système de règles obéit à deux propriétés très importantes :

  1. La complétude : Chaque proposition valide, chaque tautologie, peut être démontrée à l'aide de ces règles. Toute proposition valide peut être démontrée.
  2. La correction : Chaque démonstration est correcte, c'est-à-dire que si l'on suit les règles alors toute proposition démontrée est valide. Chaque proposition prouvée est bel et bien une tautologie.
Ces deux propriétés sont appelées complétude et correction. Elles établissent que la déduction naturelle est une façon assurée et correcte de démontrer la validité d'une proposition.

La propriété de complétude a été prouvée par le mathématicien suisse Paul Bernays.