Déduction naturelle - Définition

Les règles fondamentales de la déduction naturelle

Les propositions au-dessus de la barre s'appellent les prémisses et la proposition sous la barre s'appelle la conclusion. La règle ci-dessus élimine le connecteur →. En fait, dans la déduction naturelle, il y a deux types de règles: des règles d'introduction et des règles d'élimination. Nous allons, dans un premier temps, présenter les règles qui régissent les connecteurs →, ∧ et ⊥.

L'hypothèse

Les règles d'introduction

Dans la règle d'introduction de la flèche l'hypothèse p est déchargée, ce qui se dénote en la mettant entre crochets.

Le règles d'élimination

Les règles qui régissent ⊥ (faux)

Ce sont deux règles qui éliminent ⊥, mais qui ont la particularité d'introduire une proposition. Comme souvent, on utilise la notation ¬p comme une abréviation de p → ⊥.

La règle de de raisonnement par l'absurde (reductio ad absurdum) décharche également une hypothèse.

La signification des règles

Si l'on a une démonstration de p et une démonstration de q, on a une démonstration de p ∧ q, c'est ce que qu'énonce la règle (∧ I). La règle (→ I) dit que si de l'hypothèse p on peut déduire q alors on peut déduire p → q, l'hypothèse p est alors enlevée de l'ensemble des hypothèses, on dit qu'elle est déchargée. Les deux règles d'élimination du connecteur ∧ énonce que si l'on a une démonstration de p ∧ q on a immédiatement une démonstration de p (première règle) et on a aussi une démonstration de q (deuxième règle). La règle d'élimination de → est le modus ponens bien connu depuis Aristote. La règle (⊥) énonce le fait que de la proposition fausse on peut déduire n'importe quelle autre proposition. La règle (RAA) est celle du raisonnement par l'absurde, c'est elle qui donne à la déduction naturelle son caractère non intuitionniste (c'est-à-dire « classique »), dans ce cas l'hypothèse ¬ p est déchargée. On remarquera cependant que si la règle (⊥) peut être vue comme une règle d'élimination du connecteur ⊥, la règle (RAA) n'est pas une règle d'élimination, encore moins une règle d'introduction, on voit donc que cette règle créée un biais dans la régularité introduction-élimination de la déduction naturelle intuitionniste.

La page Calcul des propositions donne une variante de la déduction naturelle avec des séquents spécifiques, dit « naturels », où les hypothèses sont gardées comme un contexte et où les hypothèses n'ont pas à être déchargées, mais disparaissent du contexte.

Quelques exemples

• Soit à démontrer p ∧ q → q ∧ p.

Les deux hypothèses sont déchargées par la règle .

• Démontrons ¬¬p → p autrement dit ((p → ⊥) → ⊥) → p.

Ici les deux hypothèses sont déchargées chacune par une règle différente : l'hypothèse est déchargée par la règle d'introduction de la flèche, l'hypothèse par la règle de raisonnement par l'absurde.

Les autres connecteurs et les quantificateurs

Les règles de la disjonction

Introduction

Élimination

Cette règle décharge les deux hypothèse p et q.

Les règles de la quantification universelle

En ce qui concerne la syntaxe, nous renvoyons à l'article calcul des prédicats. Nous ne donnons que les règles.

Introduction

à condition que la variable x n'apparaisse dans aucune des hypothèses non déchargées.

Élimination

Les règles de la quantification existentielle

Introduction

Élimination

Cette règle décharge l'hypothèse P

On notera l'analogie qui n'est pas fortuite entre les règles du connecteur et du quantificateur , d'une part, et du connecteur et du quantificateur d'autre part.

Coupure en déduction naturelle